Crumbling Abstract Machines

Beniamino Accattoli, Andrea Condoluci, Giulio Guerrieri, Claudio Sacerdoti Coen

Research output: Chapter or section in a book/report/conference proceedingChapter in a published conference proceeding

14 Citations (SciVal)

Abstract

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.

Original languageEnglish
Title of host publicationProceedings of the 21st International Symposium on Principles and Practice of Declarative Programming, PPDP 2019
Subtitle of host publicationPorto, Portugal, October 7-9, 2019
PublisherAssociation for Computing Machinery
Pages4:1-4:15
Number of pages15
ISBN (Electronic)9781450372497
DOIs
Publication statusPublished - 7 Oct 2019
Event21st International Symposium on Principles and Practice of Declarative Programming, PPDP 2019 - Porto, Portugal
Duration: 7 Oct 20199 Oct 2019

Publication series

NameACM International Conference Proceeding Series

Conference

Conference21st International Symposium on Principles and Practice of Declarative Programming, PPDP 2019
Country/TerritoryPortugal
CityPorto
Period7/10/199/10/19

Funding

Acknowledgments. This work has been partially funded by the ANR JCJC grant COCA HOLA (ANR-16-CE40-004-01) and by the EPSRC grant EP/R029121/1 “Typed Lambda-Calculi with Sharing and Unsharing”.

Keywords

  • Abstract machine
  • Complexity
  • Explicit substitution
  • Lambda-calculus

ASJC Scopus subject areas

  • Human-Computer Interaction
  • Computer Networks and Communications
  • Computer Vision and Pattern Recognition
  • Software

Fingerprint

Dive into the research topics of 'Crumbling Abstract Machines'. Together they form a unique fingerprint.

Cite this