A Functional Correspondence between Evaluators and Abstract Machines

• DOI: 10.7146/brics.v10i13.21783
• Publication Date: 2016-02-22T06:45:16Z
• Authors: Mads Sig Ager; Dariusz Biernacki; Olivier Danvy; Jan Midtgaard
• Keywords: Abstract machine

We bridge the gap between functional evaluators and abstract machines for lambda-calculus, using closure conversion, transformation into continuation-passing style, defunctionalization of continuations.<br /> <br />We illustrate this by deriving Krivine's machine from an ordinary call-by-name evaluator call-by-value Felleisen et al.'s CEK machine. The first derivation is strikingly simpler than what can be found in literature. second one new. Together, they show that correspond to facets lambda-calculus.<br then reveal denotational content Hannan Miller's CLS Landin's SECD formally compare corresponding we some relative degrees freedom design spaces lambda-calculus with computational effects.<br />For purpose work, distinguish virtual machines, which have instruction set, do not. Categorical Abstract Machine, example, has but machine, not; directly operate on lambda-terms instead. present corresponds Machine.