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

Tom Gundersen, Willem Heijltjes, Michel Parigot

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

2 Citations (Scopus)
20 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 languageEnglish
Title of host publicationLogic for Programming, Artificial Intelligence, and Reasoning (LPAR)
Subtitle of host publicationProceedings of the 19th International Conference, LPAR, Stellenbosch, South Africa, December 14-19, 2013
Place of PublicationHeidelberg, Germany
PublisherSpringer
Pages340-354
Number of pages15
ISBN (Print)9783642452208
DOIs
Publication statusPublished - 1 Jan 2013
EventLPAR: International Conferences on Logic for Programming, Artificial Intelligence and Reasoning - Stellenbosch, South Africa
Duration: 15 Nov 2013 → …

Publication series

NameLecture Notes in Computer Science
Volume8312

Conference

ConferenceLPAR: International Conferences on Logic for Programming, Artificial Intelligence and Reasoning
CountrySouth Africa
CityStellenbosch
Period15/11/13 → …

Fingerprint Dive into the research topics of 'A proof of strong normalisation of the typed atomic lambda-calculus'. Together they form a unique fingerprint.

Cite this