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

}