Implementing open call-by-value

DOI10.1007/978-3-319-68972-2_1MaRDI QIDQ2093145zbMATH OpenOpenAlexFDO

Authors Beniamino Accattoli, Giulio Guerrieri

Publication date 4 November 2022

Full work available at URL https://arxiv.org/abs/1701.08186

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Abstract: The theory of the call-by-value lambda-calculus relies on weak evaluation and closed terms, that are natural hypotheses in the study of programming languages. To model proof assistants, however, strong evaluation and open terms are required. Open call-by-value is the intermediate setting of weak evaluation with open terms, on top of which Gr'egoire and Leroy designed the abstract machine of Coq. This paper provides a theory of abstract machines for open call-by-value. The literature contains machines that are either simple but inefficient, as they have an exponential overhead, or efficient but heavy, as they rely on a labelling of environments and a technical optimization. We introduce a machine that is simple and efficient: it does not use labels and it implements open call-by-value within a bilinear overhead. Moreover, we provide a new fine understanding of how different optimizations impact on the complexity of the overhead.

Recommendations

• Open call-by-value
• A reflection on call-by-value
• scientific article; zbMATH DE number 512793
• Call-by-value Solvability
• Call-by-value solvability, revisited
• Call-by-value, call-by-name and the logic of values
• Call-by-push-value: Decomposing call-by-value and call-by-name
• Call-By-Value, Again!
• From call-by-value to interaction by typed closure conversion
• Lazy call-by-value evaluation

Cited in

(8)

• (In)efficiency and reasonable cost models
• Open call-by-value
• The Negligible and Yet Subtle Cost of Pattern Matching
• A Fresh Look at the λ-Calculus
• Deriving an abstract machine for strong call by need
• Types of fireballs
• A fresh inductive approach to useful call-by-value
• A reversible crumbling abstract machine for Plotkin's call-by-value

This page was built for publication: Implementing open call-by-value

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2093145)