Why the usual candidates of reducibility do not work for the symmetric $\lambda \mu$-calculus

Abstract

The symmetric $\lambda mu$-calculus is the $\lambda \mu$-calculus introduced by Parigot in which the reduction rule ${\mu }^{\prime }$, which is the symmetric of $\mu$, is added. We give examples explaining why the technique using the usual candidates of reducibility does not work. We also prove a standardization theorem for this calculus.

Second Workshop on Computational Logic and Applications (CLA 2004), France (2004)

References in corpus (1)

• A short proof of the strong normalization of the simply typed $\lambda \mu$-calculus