TY - RPRT

T1 - The lambda sigma calculus and strong normalization

AU - Schack-Nielsen, Anders

AU - Schürmann, Carsten

N1 - TR-2011-150

PY - 2011

Y1 - 2011

N2 - 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.

AB - 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.

M3 - Report

SN - 978-87-7949-249-3

BT - The lambda sigma calculus and strong normalization

PB - IT-Universitetet i København

ER -