Abstract Machines for Open Call-by-Value

Beniamino Accattoli, Giulio Guerrieri

Research output: Contribution to journalArticle

Abstract

The theory of the call-by-value λ-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 (possibly) open terms, on top of which Grégoire and Leroy designed one of the abstract machines of Coq. This paper provides a theory of abstract machines for the fireball calculus, the simplest presentation of 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 labeling of environments and a technical optimization. We introduce a machine that is simple and efficient: it does not use labels and it implements the fireball calculus within a bilinear overhead. Moreover, we provide a new fine understanding of how different optimizations impact on the complexity of the overhead, and evidence that the time cost model we work with is minimal.
Original languageEnglish
Article number102275
JournalScience of Computer Programming
Volume184
Early online date15 Mar 2019
DOIs
Publication statusPublished - 1 Oct 2019

Fingerprint Dive into the research topics of 'Abstract Machines for Open Call-by-Value'. Together they form a unique fingerprint.

Cite this