A Strong Distillery
Beniamino Accattoli, Pablo Barenbaum, Damiano Mazza

TL;DR
This paper introduces a new abstract machine for strong evaluation of lambda-terms, specifically for leftmost-outermost evaluation to normal form, with proven correctness, completeness, and linear overhead, enhancing understanding of implementation strategies in proof assistants.
Contribution
It presents the Strong Milner Abstract Machine, a novel variant of the KAM for strong evaluation, with a detailed analysis of its properties and overhead, and introduces a decoding method into the Linear Substitution Calculus.
Findings
The machine is correct and complete for leftmost-outermost evaluation.
Overhead is linear in steps and initial term size.
Features backtracking phases and their interactions with abstractions.
Abstract
Abstract machines for the strong evaluation of lambda-terms (that is, under abstractions) are a mostly neglected topic, despite their use in the implementation of proof assistants and higher-order logic programming languages. This paper introduces a machine for the simplest form of strong evaluation, leftmost-outermost (call-by-name) evaluation to normal form, proving it correct, complete, and bounding its overhead. Such a machine, deemed Strong Milner Abstract Machine, is a variant of the KAM computing normal forms and using just one global environment. Its properties are studied via a special form of decoding, called a distillation, into the Linear Substitution Calculus, neatly reformulating the machine as a standard micro-step strategy for explicit substitutions, namely linear leftmost-outermost reduction, i.e., the extension to normal form of linear head reduction. Additionally, the…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · semigroups and automata theory · Logic, Reasoning, and Knowledge
