Unpublished

Abstract

A completeness result for Lambda-Mu
by S. van Bakel.

We study the expressivity of Parigot's Lambda-Mu-calculus, and show that each statement that is provable in Gentzen's LK has a proof in Lambda-Mu. This result is obtained through defining an interpretation from nets from the X-calculus into both the lambda-calculus and Lambda-Mu; X enjoys the full Curry-Howard isomorphism for (the implicative fragment of) LK, and cut-elimination in LK is represented by reduction in X. This interpretation will be shown to preserve reduction in X via equality in the target calculi, and to preserve typeability using the standard double negation translation technique of types. Using the fact that, in Lambda-Mu, we can inhabit $\neg \neg A \arrow A$ for all types $A$, a completeness result as well as a consistency result are shown for Lambda-Mu.

ps pdf