Crumbling Abstract Machines
| Autor: | Claudio Sacerdoti Coen, Beniamino Accattoli, Giulio Guerrieri, Andrea Condoluci |
|---|---|
| Přispěvatelé: | Proof search and reasoning with logic specifications (PARSIFAL), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Dipartimento di Informatica - Scienza e Ingegneria [Bologna] (DISI), Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO), Department of Computer Science [Bath], University of Bath [Bath], Department of Computer Science and Engineering [Bologna] (DISI), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Accattoli, Beniamino, Condoluci, Andrea, Guerrieri, Giulio, Coen, Claudio Sacerdoti |
| Jazyk: | angličtina |
| Rok vydání: | 2019 |
| Předmět: |
FOS: Computer and information sciences
Computer Science - Logic in Computer Science Theoretical computer science Computer science Context (language use) 02 engineering and technology Open Call By Value Reduction Machines Crumbling Graph Reduction Abstract machine 020204 information systems 0202 electrical engineering electronic engineering information engineering Lambda-calculus 03B70 68N18 03B40 Representation (mathematics) Computer Science - Programming Languages Explicit substitution [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 020207 software engineering Construct (python library) Complexity Data structure Logic in Computer Science (cs.LO) Iterated function Graph reduction Inefficiency Programming Languages (cs.PL) |
| Zdroj: | PPDP 2019-21st International Symposium on Principles and Practice of Programming Languages PPDP 2019-21st International Symposium on Principles and Practice of Programming Languages, Oct 2019, Porto, Portugal. ⟨10.1145/3354166.3354169⟩ PPDP |
| DOI: | 10.1145/3354166.3354169⟩ |
| Popis: | International audience; Extending the λ-calculus with a construct for sharing, such as let expressions, enables a special representation of terms: iterated applications are decomposed by introducing sharing points in between any two of them, reducing to the case where applications have only values as immediate subterms. This work studies how such a crumbled representation of terms impacts on the design and the efficiency of abstract machines for call-by-value evaluation. About the design, it removes the need for data structures encoding the evaluation context, such as the applicative stack and the dump, that get encoded in the environment. About efficiency, we show that there is no slowdown, clarifying in particular a point raised by Kennedy, about the potential inefficiency of such a representation. Moreover, we prove that everything smoothly scales up to the delicate case of open terms, needed to implement proof assistants. Along the way, we also point out that continuation-passing style transformations-that may be alternatives to our representation-do not scale up to the open case. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|