💾 Archived View for dcreager.net › papers › Baker1994.gmi captured on 2024-06-16 at 12:31:42. Gemini links have been rewritten to link to archived content
⬅️ Previous capture (2024-02-05)
-=-=-=-=-=-=-
Henry G. Baker. “Linear logic and permutation stacks—The Forth shall be first”. ACM SIGARCH Computer Architecture News. Volume 22, Issue 1, March 1994. pp34–43
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.