Linear logic and permutation stacks—the Forth shall be first
- 1 March 1994
- journal article
- Published by Association for Computing Machinery (ACM) in ACM SIGARCH Computer Architecture News
- Vol. 22 (1) , 34-43
- https://doi.org/10.1145/181993.181999
Abstract
Girard's linear logic can be used to model programming languages in which each bound variable name has exactly one "occurrence"---i.e., no variable can have implicit "fan-out"; multiple uses require explicit duplication. Among other nice properties, "linear" languages need no garbage collector, yet have no dangling reference problems. We show a natural equivalence between a "linear" programming language and a stack machine in which the top items can undergo arbitrary permutations. Such permutation stack machines can be considered combinator abstractions of Moore's Forth programming language.Keywords
This publication has 75 references indexed in Scilit:
- A “linear logic” QuicksortACM SIGPLAN Notices, 1994
- Sparse polynomials and linear logicACM SIGSAM Bulletin, 1993
- Equal rights for functional objects or, the more things change, the more they are the sameACM SIGPLAN OOPS Messenger, 1993
- How to steal from a limited private accountACM SIGAda Ada Letters, 1993
- Metacircular semantics for common Lisp special formsACM SIGPLAN Lisp Pointers, 1992
- Lively linear LispACM SIGPLAN Notices, 1992
- Structured programming with limited private types in AdaACM SIGAda Ada Letters, 1991
- Can programming be liberated from the von Neumann style?Communications of the ACM, 1978
- Code Generation for Expressions with Common SubexpressionsJournal of the ACM, 1977
- Optimal Code Generation for Expression TreesJournal of the ACM, 1976