A proof of strong normalisation of the typed atomic lambda-calculus

Tom Gundersen; Willem Heijltjes; Michel Parigot

doi:10.1007/978-3-642-45221-5_24

A proof of strong normalisation of the typed atomic lambda-calculus

Tom Gundersen, Willem Heijltjes, Michel Parigot

Université Paris Diderot

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

4 Citations (SciVal)

76 Downloads (Pure)

Abstract

The atomic lambda-calculus is a typed lambda-calculus with explicit sharing, which originates in a Curry-Howard interpretation of a deep-inference system for intuitionistic logic. It has been shown that it allows fully lazy sharing to be reproduced in a typed setting. In this paper we prove strong normalization of the typed atomic lambda-calculus using Tait's reducibility method.

Original language	English
Title of host publication	Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)
Subtitle of host publication	Proceedings of the 19th International Conference, LPAR, Stellenbosch, South Africa, December 14-19, 2013
Place of Publication	Heidelberg, Germany
Publisher	Springer
Pages	340-354
Number of pages	15
ISBN (Print)	9783642452208
DOIs	https://doi.org/10.1007/978-3-642-45221-5_24
Publication status	Published - 1 Jan 2013
Event	LPAR: International Conferences on Logic for Programming, Artificial Intelligence and Reasoning - Stellenbosch, South Africa Duration: 15 Nov 2013 → …

Publication series

Name	Lecture Notes in Computer Science
Volume	8312

Conference

Conference	LPAR: International Conferences on Logic for Programming, Artificial Intelligence and Reasoning
Country/Territory	South Africa
City	Stellenbosch
Period	15/11/13 → …

Access to Document

10.1007/978-3-642-45221-5_24

author's version.PDF
The final publication is available at https://doi.org/10.1007/978-3-642-45221-5_24
Accepted author manuscript, 356 KB

Cite this

Gundersen, T., Heijltjes, W., & Parigot, M. (2013). A proof of strong normalisation of the typed atomic lambda-calculus. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR): Proceedings of the 19th International Conference, LPAR, Stellenbosch, South Africa, December 14-19, 2013 (pp. 340-354). (Lecture Notes in Computer Science; Vol. 8312). Springer. https://doi.org/10.1007/978-3-642-45221-5_24

A proof of strong normalisation of the typed atomic lambda-calculus. / Gundersen, Tom; Heijltjes, Willem; Parigot, Michel.
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR): Proceedings of the 19th International Conference, LPAR, Stellenbosch, South Africa, December 14-19, 2013. Heidelberg, Germany: Springer, 2013. p. 340-354 (Lecture Notes in Computer Science; Vol. 8312).

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

Gundersen, T, Heijltjes, W & Parigot, M 2013, A proof of strong normalisation of the typed atomic lambda-calculus. in Logic for Programming, Artificial Intelligence, and Reasoning (LPAR): Proceedings of the 19th International Conference, LPAR, Stellenbosch, South Africa, December 14-19, 2013. Lecture Notes in Computer Science, vol. 8312, Springer, Heidelberg, Germany, pp. 340-354, LPAR: International Conferences on Logic for Programming, Artificial Intelligence and Reasoning, Stellenbosch, South Africa, 15/11/13. https://doi.org/10.1007/978-3-642-45221-5_24

Gundersen T, Heijltjes W, Parigot M. A proof of strong normalisation of the typed atomic lambda-calculus. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR): Proceedings of the 19th International Conference, LPAR, Stellenbosch, South Africa, December 14-19, 2013. Heidelberg, Germany: Springer. 2013. p. 340-354. (Lecture Notes in Computer Science). doi: 10.1007/978-3-642-45221-5_24

Gundersen, Tom ; Heijltjes, Willem ; Parigot, Michel. / A proof of strong normalisation of the typed atomic lambda-calculus. Logic for Programming, Artificial Intelligence, and Reasoning (LPAR): Proceedings of the 19th International Conference, LPAR, Stellenbosch, South Africa, December 14-19, 2013. Heidelberg, Germany : Springer, 2013. pp. 340-354 (Lecture Notes in Computer Science).

@inproceedings{c28a6acb02584d79a794e4a828337e5c,

title = "A proof of strong normalisation of the typed atomic lambda-calculus",

abstract = "The atomic lambda-calculus is a typed lambda-calculus with explicit sharing, which originates in a Curry-Howard interpretation of a deep-inference system for intuitionistic logic. It has been shown that it allows fully lazy sharing to be reproduced in a typed setting. In this paper we prove strong normalization of the typed atomic lambda-calculus using Tait's reducibility method.",

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

year = "2013",

month = jan,

day = "1",

doi = "10.1007/978-3-642-45221-5_24",

language = "English",

isbn = "9783642452208",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "340--354",

booktitle = "Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)",

note = "LPAR: International Conferences on Logic for Programming, Artificial Intelligence and Reasoning ; Conference date: 15-11-2013",

}

TY - GEN

T1 - A proof of strong normalisation of the typed atomic lambda-calculus

AU - Gundersen, Tom

AU - Heijltjes, Willem

AU - Parigot, Michel

PY - 2013/1/1

Y1 - 2013/1/1

N2 - The atomic lambda-calculus is a typed lambda-calculus with explicit sharing, which originates in a Curry-Howard interpretation of a deep-inference system for intuitionistic logic. It has been shown that it allows fully lazy sharing to be reproduced in a typed setting. In this paper we prove strong normalization of the typed atomic lambda-calculus using Tait's reducibility method.

AB - The atomic lambda-calculus is a typed lambda-calculus with explicit sharing, which originates in a Curry-Howard interpretation of a deep-inference system for intuitionistic logic. It has been shown that it allows fully lazy sharing to be reproduced in a typed setting. In this paper we prove strong normalization of the typed atomic lambda-calculus using Tait's reducibility method.

U2 - 10.1007/978-3-642-45221-5_24

DO - 10.1007/978-3-642-45221-5_24

M3 - Chapter in a published conference proceeding

SN - 9783642452208

T3 - Lecture Notes in Computer Science

SP - 340

EP - 354

BT - Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)

PB - Springer

CY - Heidelberg, Germany

T2 - LPAR: International Conferences on Logic for Programming, Artificial Intelligence and Reasoning

Y2 - 15 November 2013

ER -

A proof of strong normalisation of the typed atomic lambda-calculus

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this