Abstract In this paper, in connection with the program of extending the Curry–Howard isomorphism to classical logic, we study the $\lambda \mu$ -calculus of Parigot emphasizing the difference between the original version of Parigot and the version of de Groote in terms of normalization properties. In order to talk about a satisfactory representation of the integers, besides the usual $\beta$ -, $\mu$ -, and $\mu '$ -reductions, we consider the $\lambda \mu$ -calculus augmented with the reduction rules $\rho$ , $\theta$ and $\varepsilon$ . We show that we need all of these rules for this purpose. Then we prove that, with the syntax of Parigot, the calculus enjoys the strong normalization property even when we add the rules $\rho$ , $\theta$ , and $\epsilon$ , while the $\lambda \mu$ -calculus presented with the more flexible de Groote-style syntax, in contrast, has only the weak normalization property. In particular, we present a normalization algorithm for the $\beta \mu \mu '\rho \theta \varepsilon$ -reduction in the de Groote-style calculus.

Expansion is a crucial operation for calculating principal typings in intersection type systems. Because the early definitions of expansion were complicated, E-variables were introduced in order to make the calculations easier to mechanise and reason

Abstract We give a direct, purely arithmetical and elementary proof of the strong normalization of the cut-elimination procedure for full (i.e., in presence of all the usual connectives) classical natural deduction.

Abstract Storage operators have been introduced by J. L. Krivine in [5] they are closed λ-terms which, for a data type, allow one to simulate a “call by value” while using the “call by name” strategy. In this paper, we introduce the directed λ-calculus and show that it has the usual properties of the ordinary λ-calculus. With this calculus we get an equivalent—and simple—definition of the storage operators that allows to show some of their properties: • the stability of the set of storage operators under the β-equivalence (Theorem 5.1.1); • the undecidability (and semidecidability) of the problem “is a closed λ-term t a storage operator for a finite set of closed normal λ-terms?” (Theorems 5.2.2 and 5.2.3); • the existence of storage operators for every finite set of closed normal λ-terms (Theorem 5.4.3); • the computation time of the “storage operation” (Theorem 5.5.2).