Abstract

The main concern of this paper is the design of a noetherian and confluent normalization for $\mathbf{LK}^2$. The method we present is powerful: since it allows us to recover as fragments formalisms as seemingly different as Girard's $\mathbf{LC}$ and Parigot's $\lambda\mu, \mathbf{FD}$, delineates other viable systems as well, and gives means to extend the Krivine/Leivant paradigm of `programming-with-proofs' to classical logic; it is painless: since we reduce strong normalization and confluence to the same properties for linear logic using appropriate embeddings ; it is unifying: it organizes known solutions in a simple pattern that makes apparent the how and why of their making. A comparison of our method to that of embedding $\mathbf{LK}$ into $\mathbf{LJ}$ brings to the fore the latter's defects for these `deconstructive purposes'.