💾 Archived View for dcreager.net › papers › McBride2018.gmi captured on 2024-08-18 at 17:54:34. Gemini links have been rewritten to link to archived content
⬅️ Previous capture (2024-06-16)
-=-=-=-=-=-=-
Conor McBride. “Everybody’s Got To Be Somewhere”. In Proceedings MSFP 2018, EPTCS 275, 2018, pp. 53-69.
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.
Other approaches where binders describe where in the underlying tree the bound name is used:
[Sato2013] Viewing λ-terms through maps
@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} }