Sciweavers

TLCA
2001
Springer

Strong Normalization of Classical Natural Deduction with Disjunction

14 years 3 months ago
Strong Normalization of Classical Natural Deduction with Disjunction
We introduce λµ→∧∨⊥ , an extension of Parigot’s λµ-calculus where disjunction is taken as a primitive. The associated reduction relation, which includes the permutative conversions related to disjunction, is Church-Rosser, strongly normalizing, and such that the normal deductions satisfy the subformula property. From a computer science point of view, λµ→∧∨⊥ may be seen as the core of a typed cbn functional language featuring product, coproduct, and control operators.
Philippe de Groote
Added 30 Jul 2010
Updated 30 Jul 2010
Type Conference
Year 2001
Where TLCA
Authors Philippe de Groote
Comments (0)