¶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.

¶Related

Other approaches where binders describe where in the underlying tree the bound name is used:

[Sato2013] Viewing λ-terms through maps

2

16

22

@article{McBride_2018,
   title={Everybody’s Got To Be Somewhere},
   volume={275},
   ISSN={2075-2180},
   url={http://dx.doi.org/10.4204/EPTCS.275.6},
   DOI={10.4204/eptcs.275.6},
   journal={Electronic Proceedings in Theoretical Computer Science},
   publisher={Open Publishing Association},
   author={McBride, Conor},
   year={2018},
   month=jul, pages={53–69} }