We introduce constructive and classical systems for nonstandard arithmetic and show how variants of the functional interpretations due to Gödel and Shoenfield can be used to rewrite proofs performed in these systems into standard ones. These functional interpretations show in particular that our nonstandard systems are conservative extensions of E-HAω and E-PAω, strengthening earlier results by Moerdijk and Palmgren, and Avigad and Helzner. We will also indicate how our rewriting algorithm can be used for term extraction purposes. To conclude the (...) paper, we will point out some open problems and directions for future research, including some initial results on saturation principles. (shrink)

We show that Shoenfield's functional interpretation of Peano arithmetic can be factorized as a negative translation due to J. L. Krivine followed by Gödel's Dialectica interpretation. (© 2007 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim).

Storage operators are λ-terms which simulate call-by-value in call-by-name for a given set of terms. Krivine's storage operator theorem shows that any term of type ¬D → ¬D*, where D* is the Gödel translation of D, is a storage operator for the terms of type D when D is a data-type or a formula with only positive second order quantifiers. We prove that a new semantical version of Krivine's theorem is valid for every types. This also gives a simpler proof (...) of Krivine's theorem using the properties of data-types. (shrink)

The storage operators were introduced by J.L. Krivine ([6]); they are closed λ-terms which, for some fixed data type (the integers for example), allow to simulate “call by value” while using “call by name”. J.L. Krivine showed that such operators can be typed, in the type system, using Gödel's translation from classical to intuitionistic logic ([8]).This paper studies the existence of storage operators which give a normal form as result (strong storage operators) for recursive and iterative representation of data in (...) λ-calculus. We obtain the following result:We can find typed strong storage operators for the recursive representations of data type, but that is not the case for the iterative representations of an infinite data type.We give the proof of this result in the case of integers. (shrink)

In 1990, J. L. Krivine introduced the notion of storage operator to simulate, for Church integers, the “call by value” in a context of a “call by name” strategy. In the present paper we define for every λ-term S which realizes the successor function on Church integers the notion of S-storage operator. We prove that every storage operator is an S-storage operator. But the converse is not always true.

We describe here a simple method in order to obtain programs from proofs in second-order classical logic. Then we extend to classical logic the results about storage operators proved by Krivine for intuitionistic logic. This work generalizes previous results of Parigot.

A numeral system is an infinite sequence of different closed normal -terms intended to code the integers in -calculus. Barendregt has shown that if we can represent, for a numeral system, the functions Successor, Predecessor, and Zero Test, then all total recursive functions can be represented. In this paper we prove the independancy of these three particular functions. We give at the end a conjecture on the number of unary functions necessary to represent all total recursive functions.

We refute the conjecture that all negative translations are intuitionistically equivalent by giving two counterexamples. Then we characterise the negative translations intuitionistically equivalent to the usual ones.

We adapt Streicher and Kohlenbach's proof of the factorization S = KD of the Shoenfield translation S in terms of Krivine's negative translation K and the Gödel functional interpretation D, obtaining a proof of the factorization U = KB of Ferreira's Shoenfield-like bounded functional interpretation U in terms of K and Ferreira and Oliva's bounded functional interpretation B.

We present a functional interpretation of Peano arithmetic that uses Gödel’s computable functionals and which systematically injects uniformities into the statements of finite-type arithmetic. As a consequence, some uniform boundedness principles are interpreted while maintaining unmoved the -sentences of arithmetic. We explain why this interpretation is tailored to yield conservation results.

In this paper, we extend the system AF2 in order to have the subject reduction for the $betaeta$-reduction. We prove that the types with positive quantifiers are complete for models that are stable by weak-head expansion.

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: $\bullet$ the stability of the set (...) of storage operators under the β-equivalence (Theorem 5.1.1); $\bullet$ 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); $\bullet$ the existence of storage operators for every finite set of closed normal λ-terms (Theorem 5.4.3); $\bullet$ the computation time of the "storage operation" (Theorem 5.5.2). (shrink)