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

Tom Gundersen; Willem Heijltjes; Michel Parigot

doi:10.1109/LICS.2013.37

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 proceeding › Chapter in a published conference proceeding

14 Citations (SciVal)

296 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 language	English
Title of host publication	Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science
Subtitle of host publication	LICS'13
Publisher	IEEE
Pages	311-320
Number of pages	10
ISBN (Print)	9781479904136
DOIs	https://doi.org/10.1109/LICS.2013.37
Publication status	Published - 1 Aug 2013
Event	Twenty-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

Name	ACM/IEEE Symposium on Logic in Computer Science
Publisher	ACM/IEEE
ISSN (Print)	1043-6871

Conference

Conference	Twenty-Eighth Annucal ACM/IEEE Symposium on Logic in Computer Science (LICS 2013)
Country/Territory	USA United States
City	New Orleans
Period	24/06/13 → 27/06/13

Access to Document

10.1109/LICS.2013.37

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

Atomic lambda-calculus: A typed lambda-calculus with explicit sharing. / Gundersen, Tom; Heijltjes, Willem; Parigot, Michel.
Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science: LICS'13. IEEE, 2013. p. 311-320 (ACM/IEEE Symposium on Logic in Computer Science).

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

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. ACM/IEEE Symposium on Logic in Computer Science, IEEE, pp. 311-320, Twenty-Eighth Annucal ACM/IEEE Symposium on Logic in Computer Science (LICS 2013), New Orleans, USA United States, 24/06/13. https://doi.org/10.1109/LICS.2013.37

@inproceedings{fce0e7f9f83944bf9f0b0716d2465d9a,

title = "Atomic lambda-calculus: A typed lambda-calculus with explicit sharing",

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.",

author = "Tom Gundersen and Willem Heijltjes and Michel Parigot",

year = "2013",

month = aug,

day = "1",

doi = "10.1109/LICS.2013.37",

language = "English",

isbn = "9781479904136 ",

series = "ACM/IEEE Symposium on Logic in Computer Science",

publisher = "IEEE",

pages = "311--320",

booktitle = "Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science",

address = "USA United States",

note = "Twenty-Eighth Annucal ACM/IEEE Symposium on Logic in Computer Science (LICS 2013) ; Conference date: 24-06-2013 Through 27-06-2013",

}

TY - GEN

T1 - Atomic lambda-calculus

T2 - Twenty-Eighth Annucal ACM/IEEE Symposium on Logic in Computer Science (LICS 2013)

AU - Gundersen, Tom

AU - Heijltjes, Willem

AU - Parigot, Michel

PY - 2013/8/1

Y1 - 2013/8/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84883443813&partnerID=8YFLogxK

UR - http://lii.rwth-aachen.de/lics/lics13/

UR - http://dx.doi.org/10.1109/LICS.2013.37

U2 - 10.1109/LICS.2013.37

DO - 10.1109/LICS.2013.37

M3 - Chapter in a published conference proceeding

AN - SCOPUS:84883443813

SN - 9781479904136

T3 - ACM/IEEE Symposium on Logic in Computer Science

SP - 311

EP - 320

BT - Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science

PB - IEEE

Y2 - 24 June 2013 through 27 June 2013

ER -

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

Abstract

Publication series

Conference

Access to Document

Other files and links

Cite this