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

Tom Gundersen, Willem Heijltjes, Michel Parigot

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

17 Citations (SciVal)
359 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)
Country/TerritoryUSA United States
CityNew Orleans
Period24/06/1327/06/13

Fingerprint

Dive into the research topics of 'Atomic lambda-calculus: A typed lambda-calculus with explicit sharing'. Together they form a unique fingerprint.

Cite this