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.

In this work, we continue our consideration of the constructions presented in the paperKrivine's Classical Realizability from a Categorical Perspectiveby Thomas Streicher. Therein, the author points towards the interpretation of the classical realizability of Krivine as an instance of the categorical approach started by Hyland. The present paper continues with the study of the basic algebraic set-up underlying the categorical aspects of the theory. Motivated by the search of a full adjunction, we introduce a new closure operator on the subsets of the stacks of an abstract Krivine structure that yields an adjunction between the corresponding application and implication operations. We show that all the constructions from ordered combinatory algebras to triposes presented in our previous work can be implemented,mutatis mutandis, in the new situation and that all the associated triposes are equivalent. We finish by proving that the whole theory can be developed using the ordered combinatory algebras with full adjunction or strong abstract Krivine structures as the basic set-up.

In this paper, we treat the specification problem in Krivine classical realizability (Krivine 2009Panoramas et synthèses27), in the case of arithmetical formulæ. In the continuity of previous works from Miquel and the first author (Guillermo 2008Jeux de réalisabilité en arithmétique classique, Ph.D. thesis, Université Paris 7; Guillermo and Miquel 2014Mathematical Structures in Computer Science, Epub ahead of print), we characterize the universal realizers of a formula as being the winning strategies for a game (defined according to the formula). In the first sections, we recall the definition of classical realizability, as well as a few technical results. In Section 5, we introduce in more details the specification problem and the intuition of the game-theoretic point of view we adopt later. We first present a game 1, that we prove to be adequate and complete if the language contains no instructions ‘quote’ (Krivine 2003Theoretical Computer Science308259–276), using interaction constants to do substitution over execution threads. We then show that as soon as the language contain ‘Quote,’ the game is no more complete, and present a second game 2that is both adequate and complete in the general case. In the last Section, we draw attention to a model-theoretic point of view and use our specification result to show that arithmetical formulæ are absolute for realizability models.

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.