Baker1994

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

=> Remarkable PDF | Original PDF | DOI

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.