Abstract We introduce the notion of implicative algebra, a simple algebraic structure intended to factorize the model-theoretic constructions underlying forcing and realizability (both in intuitionistic and classical logic). The salient feature of this structure is that its elements can be seen both as truth values and as (generalized) realizers, thus blurring the frontier between proofs and types. We show that each implicative algebra induces a (Set-based) tripos, using a construction that is reminiscent from the construction of a realizability tripos from a partial combinatory algebra. Relating this construction with the corresponding constructions in forcing and realizability, we conclude that the class of implicative triposes encompasses all forcing triposes (both intuitionistic and classical), all classical realizability triposes (in the sense of Krivine), and all intuitionistic realizability triposes built from partial combinatory algebras.

In this paper we present a semantics for a linear algebraic lambda-calculus based on realizability. This semantics characterizes a notion of unitarity in the system, answering a long standing issue. We derive from the semantics a set of typing rules for a simply-typed linear algebraic lambda-calculus, and show how it extends both to classical and quantum lambda-calculi.

We propose the new concept ofKrivine ordered combinatory algebra( $\mathcal{^KOCA}$ ) as foundation for the categorical study of Krivine's classical realizability, as initiated by Streicher (2013). We show that $\mathcal{^KOCA}$ 's are equivalent to Streicher'sabstract Krivine structuresfor the purpose of modeling higher-order logic, in the precise sense that they give rise to the same class oftriposes. The difference between the two representations is that the elements of a $\mathcal{^KOCA}$ play both the role of truth values and realizers, whereas truth values aresetsof realizers in $\mathcal{AKS}$ s. To conclude, we give a direct presentation of the realizability interpretation of a higher order language in a $\mathcal{^KOCA}$ , which showcases the dual role that is played by the elements of the $\mathcal{^KOCA}$ .

This paper deals with the specification problem in classical realizability (such as introduced by Krivine (2009 Panoramas et synthéses27)), which is to characterize the universal realizers of a given formula by their computational behaviour. After recalling the framework of classical realizability, we present the problem in the general case and illustrate it with some examples. In the rest of the paper, we focus on Peirce's law, and present two game-theoretic characterizations of its universal realizers. First, we consider the particular case where the language of realizers contains no extra instruction such as ‘quote’ (Krivine 2003 Theoretical Computer Science308 259–276). We present a first game $\mathds{G}$ 0 and show that the universal realizers of Peirce's law can be characterized as the uniform winning strategies for $\mathds{G}$ 0, using the technique of interaction constants. Then we show that in the presence of extra instructions such as ‘quote’, winning strategies for the game $\mathds{G}$ 0 are still adequate but no more complete. For that, we exhibit an example of a wild realizer of Peirce's law, that introduces a purely game-theoretic form of backtrack that is not captured by $\mathds{G}$ 0. We finally propose a more sophisticated game $\mathds{G}$ 1, and show that winning strategies for the game $\mathds{G}$ 1 are both adequate and complete in the general case, without any further assumption about the instruction set used by the language of classical realizers.

This paper is a study of the forcing translation through the proofs as programs correspondence in classical logic, following the methodology introduced by Krivine in . For that, we introduce an extension of (classical) higher-order arithmetic suited to express the forcing translation, called PA ω+. We present the proof system of PA ω+- based on Curry-style proof terms with call/cc - as well as the corresponding classical realizability semantics. Then, given a poset of conditions (represented in PA ω+as an upwards closed subset of a fixed meet semi-lattice), we define the forcing translation A ⇒ (p ⊢ A) (where A ranges over propositions) and show that the corresponding transformation of proofs is induced by a simple program transformation t ⇒ t* defined on raw proof-terms (i.e. independently from the derivation). From an analysis of the computational behavior of transformed programs, we show how to avoid the cost of the transformation by introducing an extension of Krivine's abstract machine devoted to the execution of proofs constructed by forcing. We show that this machine induces new classical realizability models and present the corresponding adequacy results.

Abstract We present an extension of the λ(η)-calculus with a case construct that propagates through functions like a head linear substitution, and show that this construction permits to recover the expressiveness of ML-style pattern matching. We then prove that this system enjoys the Church–Rosser property using a semi-automatic ‘divide and conquer’ technique by which we determine all the pairs of commuting subsystems of the formalism (considering all the possible combinations of the nine primitive reduction rules). Finally, we prove a separation theorem similar to Böhm's theorem for the whole formalism.

We introduce a novel model based on coherence spaces for interpreting large impredicative type systems such as the Extended Calculus of Constructions (ECC). Moreover we show that this model is well-suited for interpreting intersection types and subtyping too, and we illustrate this by interpreting a variant of ECC with an additional intersection type binder. Furthermore, we propose a general method for interpreting the impredicative level in a non-syntactical way, by allowing the model to be parametrized by an arbitrarily large coherence space in order to interpret inhabitants of impredicative types. As an application, we show that uncountable types such as the type of real numbers or Zermelo-Frankel sets can safely be axiomatized on the impredicative level of, say, ECC, without harm for consistency.