The lambda sigma calculus and strong normalization

Anders Schack-Nielsen, Carsten Schürmann

Publikation: Bog / Antologi / Rapport / Ph.D.-afhandlingRapportForskning


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.
ForlagIT-Universitetet i København
Antal sider13
ISBN (Trykt) 978-87-7949-249-3
StatusUdgivet - 2011


Dyk ned i forskningsemnerne om 'The lambda sigma calculus and strong normalization'. Sammen danner de et unikt fingeraftryk.