---
abstract: 'We prove the strong normalization of full classical natural deduction (i.e. with conjunction, disjunction and permutative conversions) by using a translation into the simply typed $\l\m$-calculus. We also extend Mendler’s result on recursive equations to this system.'
---

[**Strong normalization results by translation**]{}\

[**René DAVID and Karim NOUR**]{}\
LAMA - Equipe LIMD\
Université de Chambéry\
73376 Le Bourget du Lac\
e-mail: {david,nour}@univ-savoie.fr\

Introduction
============

It is well known that, when the underlying logic is the classical one (i.e. the absurdity rule is allowed) the connectives $\ou$ and $\et$ are redundant (they can be coded by using $\f$ and $\perp$). From a logical point of view, considering the full logic is thus somehow useless. However, from the computer science point of view, considering the full logic is interesting because, by the so-called Curry-Howard correspondence, formulas can be seen as types for functional programming languages and correct programs can be extracted from proofs. The connectives $\et$ and $\ou$ have a functional counter-part ($\et$ corresponds to a product and $\ou$ to a co-product, i.e. a [*case of*]{}) and it is thus useful to have them as primitive.

In this paper, we study the typed $\l\m^{\f\et\ou}$-calculus. This calculus, introduced by de Groote 