Atomic lambda-calculus: A typed lambda-calculus with explicit sharing

Tom Gundersen, Willem Heijltjes, Michel Parigot

Research output: Chapter in Book/Report/Conference proceedingConference contribution

8 Citations (Scopus)
154 Downloads (Pure)

Abstract

An explicit-sharing lambda-calculus is presented, based on a Curry-Howard-style interpretation of the deep inference proof formalism. Duplication of subterms during reduction proceeds `atomically', i.e. on individual constructors, similar to optimal graph reduction in the style of Lamping. The calculus preserves strong normalisation with respect to the lambda-calculus, and achieves fully lazy sharing.
Original languageEnglish
Title of host publicationProceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science
Subtitle of host publicationLICS'13
PublisherIEEE
Pages311-320
Number of pages10
ISBN (Print)9781479904136
DOIs
Publication statusPublished - 1 Aug 2013
EventTwenty-Eighth Annucal ACM/IEEE Symposium on Logic in Computer Science (LICS 2013) - New Orleans, USA United States
Duration: 24 Jun 201327 Jun 2013

Publication series

NameACM/IEEE Symposium on Logic in Computer Science
PublisherACM/IEEE
ISSN (Print)1043-6871

Conference

ConferenceTwenty-Eighth Annucal ACM/IEEE Symposium on Logic in Computer Science (LICS 2013)
CountryUSA United States
CityNew Orleans
Period24/06/1327/06/13

    Fingerprint

Cite this

Gundersen, T., Heijltjes, W., & Parigot, M. (2013). Atomic lambda-calculus: A typed lambda-calculus with explicit sharing. In Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science: LICS'13 (pp. 311-320). (ACM/IEEE Symposium on Logic in Computer Science). IEEE. https://doi.org/10.1109/LICS.2013.37