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

  • 7 Citations

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.
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
ISBN (Print)9781479904136
DOIs
StatusPublished - Jun 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

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

preserve
normalisation

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). IEEE. https://doi.org/10.1109/LICS.2013.37

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.

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

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. 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
Gundersen T, Heijltjes W, Parigot M. 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. IEEE. 2013. p. 311-320 https://doi.org/10.1109/LICS.2013.37
Gundersen, Tom ; Heijltjes, Willem ; Parigot, Michel. / Atomic lambda-calculus : A typed lambda-calculus with explicit sharing. Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science: LICS'13. IEEE, 2013. pp. 311-320
@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 = "6",
doi = "10.1109/LICS.2013.37",
language = "English",
isbn = "9781479904136",
pages = "311--320",
booktitle = "Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science",
publisher = "IEEE",
address = "USA United States",

}

TY - GEN

T1 - Atomic lambda-calculus

T2 - A typed lambda-calculus with explicit sharing

AU - Gundersen, Tom

AU - Heijltjes, Willem

AU - Parigot, Michel

PY - 2013/6

Y1 - 2013/6

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 - Conference contribution

SN - 9781479904136

SP - 311

EP - 320

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

PB - IEEE

ER -