This research paper in mathematical logic is devoted to the lambda-mu calculus of Parigot, completed by the so-called symmetric structural reduction rules, but without the extraction operator; the calculus is exposed in paragraph 2.

The main result is a very general theorem of strong normalization (theorem 25, at the end of paper). The efficiency of such a theorem is illustrated by the example of existential assertions (cf. theorem 5): if it is provable that there is an x such that A(x), the normal deduction must contain a first order term t that satisfies A. But there is a cost: the calculus is highly nondeterministic, and if theorem 25 proves that a strong normalization exists for each term, its proof uses very noneffective tools, such as König’s Lemma (cf. proposition 9), or transfinite induction up to the first uncountable ordinal.