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

Tom Gundersen, Willem Heijltjes, Michel Parigot

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

9 Citations (Scopus)
189 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 2013 → 27 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/13 → 27/06/13

Access to Document

  • AL

    © 2013 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.

    Accepted author manuscript, 257 KB

    Cite this