%0 Conference Paper
%F Oral 
%T Implementing Open Call-by-Value
%+ Proof search and reasoning with logic specifications (PARSIFAL)
%+ Institut de Mathématiques de Marseille (I2M)
%A Accattoli, Beniamino
%A Guerrieri, Giulio
%< avec comité de lecture
%3 Lecture Notes in Computer Science
%B 7th International Conference on Fundamentals of Software Engineering (FSEN)
%C Teheran, Iran
%Y Mehdi Dastani
%Y Marjan Sirjani
%I Springer International Publishing
%S Fundamentals of Software Engineering
%V LNCS-10522
%P 1-19
%8 2017-04-26
%D 2017
%R 10.1007/978-3-319-68972-2_1
%Z Computer Science [cs]/Logic in Computer Science [cs.LO]Conference papers
%X 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. This work is part of a wider research effort, the COCA HOLA project https://sites.google.com/site/beniaminoaccattoli/coca-hola.
%G English
%Z TC 2
%Z WG 2.2
%2 https://hal.science/hal-01675365/document
%2 https://hal.science/hal-01675365/file/Accattoli%2C%20Guerrieri%20-%20Implementing%20Open%20CbV.pdf
%L hal-01675365
%U https://hal.science/hal-01675365
%~ X
%~ CNRS
%~ INRIA
%~ UNIV-AMU
%~ LIX
%~ LIX-PARSIFAL
%~ INRIA-SACLAY
%~ EC-MARSEILLE
%~ INSMI
%~ X-LIX
%~ X-DEP
%~ X-DEP-INFO
%~ INRIA_TEST
%~ TESTALAIN1
%~ I2M
%~ I2M-2014-
%~ IFIP-LNCS
%~ IFIP
%~ INRIA2
%~ IFIP-TC
%~ IFIP-TC2
%~ IFIP-WG2-2
%~ IFIP-FSEN
%~ UNIV-PARIS-SACLAY
%~ INRIA-SACLAY-2015
%~ X-SACLAY
%~ INRIA2017
%~ IFIP-LNCS-10522
%~ ANR
%~ GS-COMPUTER-SCIENCE