ITU

The lambda sigma calculus and strong normalization

Research output: Book / Anthology / Report / Ph.D. thesisReportResearch

View graph of relations

Explicit substitution calculi can be classified into several dis- tinct categories depending on whether they are confluent, meta-confluent, strong normalization preserving, strongly normalizing, simulating, fully compositional, and/or local. In this paper we present a variant of the λσ-calculus, which satisfies all seven conditions. In particular, we show how to circumvent Mellies counter-example to strong normalization by a slight restriction of the congruence rules. The calculus is implemented as the core data structure of the Celf logical framework. All meta-theoretic aspects of this work have been mechanized in the Abella proof assistant.
Original languageEnglish
PublisherIT-Universitetet i København
Number of pages13
ISBN (Print) 978-87-7949-249-3
Publication statusPublished - 2011

Bibliographical note

TR-2011-150

ID: 32757144