The lambda sigma-Calculus and Strong Normalization
TR-2011-150, Anders Schack-Nielsen and Carsten Schürmann
The lambda sigma-Calculus and Strong Normalization
Anders Schack-Nielsen
Carsten Schürmann
Decmember 2011
Abstract
Explicit substitution calculi can be classified into several distinct 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 lambda sigma-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.
Technical report TR-2011-150 in IT University Technical Report Series, December 2011.
Available as PDF.