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.

• Type: Conference
• Year: 2001
• Where: TLCA
• Authors: Philippe de Groote
• Keywords: Associated Reduction Relation, Cbn Functional Language, Strongly Normalizing, Theoretical Computer Science, TLCA 2001