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 open terms, on top of which Grégoire 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.
| Original language | English |
|---|---|
| Title of host publication | Fundamentals of Software Engineering - 7th International Conference, FSEN 2017, Revised Selected Papers |
| Editors | Marjan Sirjani, Mehdi Dastani, Marjan Sirjani |
| Publisher | Springer Verlag |
| Pages | 1-19 |
| Number of pages | 19 |
| ISBN (Print) | 9783319689715 |
| DOIs | |
| Publication status | Published - 11 Oct 2017 |
| Event | 7th International Conference on Fundamentals of Software Engineering, FSEN 2017 - Teheran, Iran, Islamic Republic of Duration: 26 Apr 2017 → 28 Apr 2017 |
Publication series
| Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
|---|---|
| Volume | 10522 LNCS |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Conference
| Conference | 7th International Conference on Fundamentals of Software Engineering, FSEN 2017 |
|---|---|
| Country | Iran, Islamic Republic of |
| City | Teheran |
| Period | 26/04/17 → 28/04/17 |
ASJC Scopus subject areas
- Theoretical Computer Science
- Computer Science(all)
Cite this
Implementing Open Call-by-Value. / Accattoli, Beniamino; Guerrieri, Giulio.
Fundamentals of Software Engineering - 7th International Conference, FSEN 2017, Revised Selected Papers. ed. / Marjan Sirjani; Mehdi Dastani; Marjan Sirjani. Springer Verlag, 2017. p. 1-19 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10522 LNCS).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
}
TY - GEN
T1 - Implementing Open Call-by-Value
AU - Accattoli, Beniamino
AU - Guerrieri, Giulio
PY - 2017/10/11
Y1 - 2017/10/11
N2 - 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 open terms, on top of which Grégoire 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.
AB - 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 open terms, on top of which Grégoire 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.
UR - http://www.scopus.com/inward/record.url?scp=85032861128&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-68972-2_1
DO - 10.1007/978-3-319-68972-2_1
M3 - Conference contribution
SN - 9783319689715
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 1
EP - 19
BT - Fundamentals of Software Engineering - 7th International Conference, FSEN 2017, Revised Selected Papers
A2 - Sirjani, Marjan
A2 - Dastani, Mehdi
A2 - Sirjani, Marjan
PB - Springer Verlag
ER -