Related papers: A Classical Realizability Model arising from a Sta…
This paper is about the bar recursion operator in the context of classical realizability. After the pioneering work of Berardi, Bezem & Coquand [1], T. Streicher has shown [10], by means of their bar recursion operator, that the…
We describe a realizability framework for classical first-order logic in which realizers live in (a model of) typed {\lambda}{\mu}-calculus. This allows a direct interpretation of classical proofs, avoiding the usual negative translation to…
J.L. Krivine developed a new method based on realizability to construct models of set theory where the axiom of choice fails. We attempt to recreate his results in classical settings, i.e. symmetric extensions. We also provide a new…
During the last twenty years or so a wide range of realizability interpretations of classical analysis have been developed. In many cases, these are achieved by extending the base interpreting system of primitive recursive functionals with…
We present a new type system with support for proofs of programs in a call-by-value language with control operators. The proof mechanism relies on observational equivalence of (untyped) programs. It appears in two type constructors, which…
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…
The theory of classical realizability is a framework in which we can develop the proof-program correspondence. Using this framework, we show how to transform into programs the proofs in classical analysis with dependent choice and the…
We show how the language of Krivine's classical realizability may be used to specify various forms of nondeterminism and relate them with properties of realizability models. More specifically, we introduce an abstract notion of…
We prove the following completeness result about classical realizability: given any Boolean algebra with at least two elements, there exists a Krivine-style classical realizability model whose characteristic Boolean algebra is elementarily…
We define a variant of realizability where realizers are pairs of a term and a substitution. This variant allows us to prove the normalization of a simply-typed call-by-need $$\lambda$-$calculus with control due to Ariola et al. Indeed, in…
We use the technique of "classical realizability" to build new models of ZF + DC in which R is not well ordered. This gives new relative consistency results, probably not obtainable by forcing. This gives also a new method to get programs…
In a recent paper, Herbelin developed a calculus dPA$^\omega$ in which constructive proofs for the axioms of countable and dependent choices could be derived via the encoding of a proof of countable universal quantification as a stream of…
Realizability, introduced by Kleene, can be understood as a concretization of the Brouwer-Heyting-Kolmogorov (BHK) interpretation of proofs, providing a framework to interpret mathematical statements and proofs in terms of their…
In an impressive series of papers, Krivine showed at the edge of the last decade how classical realizability provides a surprising technique to build models for classical theories. In particular, he proved that classical realizability…
We present the guarded lambda-calculus, an extension of the simply typed lambda-calculus with guarded recursive and coinductive types. The use of guarded recursive types ensures the productivity of well-typed programs. Guarded recursive…
Based on an analysis of the inference rules used, we provide a characterization of the situations in which classical provability entails intuitionistic provability. We then examine the relationship of these derivability notions to uniform…
We extend the classical notion of solvability to a lambda-calculus equipped with pattern matching. We prove that solvability can be characterized by means of typability and inhabitation in an intersection type system P based on…
For those of us who generally live in the world of syntax, semantic proof techniques such as reducibility, realizability or logical relations seem somewhat magical despite -- or perhaps due to -- their seemingly unreasonable effectiveness.…
In this article, we investigate the arithmetical hierarchy from the perspective of realizability theory. An experimental observation in classical computability theory is that the notion of degrees of unsolvability for natural arithmetical…
The method of realizability was first developed by Kleene and is seen as a way to extract computational content from mathematical proofs. Traditionally, these models only satisfy intuitionistic logic, however this method was extended by…