Related papers: Learning, Realizability and Games in Classical Ari…
We apply to the semantics of Arithmetic the idea of ``finite approximation'' used to provide computational interpretations of Herbrand's Theorem, and we interpret classical proofs as constructive proofs (with constructive rules for $\vee,…
We prove that interactive learning based classical realizability (introduced by Aschieri and Berardi for first order arithmetic) is sound with respect to Coquand game semantics. In particular, any realizer of an…
In this paper we treat the specification problem in classical realizability (as defined in [20]) in the case of arithmetical formul{\ae}. In the continuity of [10] and [11], we characterize the universal realizers of a formula as being 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…
The present paper introduces a novel notion of `(effective) computability', called viability, of strategies in game semantics in an intrinsic (i.e., without recourse to the standard Church-Turing computability), non-inductive and…
In this dissertation we collect some results about "interactive realizability", a realizability semantics that extends the Brouwer-Heyting-Kolmogorov interpretation to (sub-)classical logic, more precisely to first-order intuitionistic…
We propose a realizability interpretation of a system for quantifier free arithmetic which is equivalent to the fragment of classical arithmetic without "nested" quantifiers, called here EM1-arithmetic. We interpret classical proofs as…
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…
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…
We show how to extract a monotonic learning algorithm from a classical proof of a geometric statement by interpreting the proof by means of interactive realizability, a realizability sematics for classical logic. The statement is about the…
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.…
We consider interactive learning in the realizable setting and develop a general framework to handle problems ranging from best arm identification to active classification. We begin our investigation with the observation that agnostic…
Machine learning researchers and practitioners steadily enlarge the multitude of successful learning models. They achieve this through in-depth theoretical analyses and experiential heuristics. However, there is no known general-purpose…
We give a new presentation of interactive realizability with a more explicit syntax. Interactive realizability is a realizability semantics that extends the Curry-Howard correspondence to (sub-)classical logic, more precisely to first-order…
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 an extension to the $\mathtt{mathlib}$ library of the Lean theorem prover formalizing the foundations of computability theory. We use primitive recursive functions and partial recursive functions as the main objects of study, and…
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…
Transfer learning is an emerging and popular paradigm for utilizing existing knowledge from previous learning tasks to improve the performance of new ones. Despite its numerous empirical successes, theoretical analysis for transfer learning…
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…
The present paper constructs three new systems of clarithmetic (arithmetic based on computability logic --- see http://www.cis.upenn.edu/~giorgi/cl.html): CLA8, CLA9 and CLA10. System CLA8 is shown to be sound and extensionally complete…