Related papers: Interactive Learning Based Realizability and 1-Bac…
In this dissertation we provide mathematical evidence that the concept of learning can be used to give a new and intuitive computational semantics of classical proofs in various fragments of Predicative Arithmetic. First, we extend Kreisel…
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…
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 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…
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 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…
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…
We analyze Coquand's game-theoretic interpretation of Peano Arithmetic through the lens of elementary descent recursion. In Coquand's game semantics, winning strategies correspond to infinitary cut-free proofs and cut elimination…
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…
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…
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 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…
In this paper, we present an interactive semantics for derivations in an infinitary extension of classical logic. The formulas of our language are possibly infinitary trees labeled by propositional variables and logical connectives. We show…
Given a dynamic ordinal game, we deem a strategy sequentially rational if there exist a Bernoulli utility function and a conditional probability system with respect to which the strategy is a maximizer. We establish a complete class theorem…
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…
Interactive-Grounded Learning (IGL) [Xie et al., 2021] is a powerful framework in which a learner aims at maximizing unobservable rewards through interacting with an environment and observing reward-dependent feedback on the taken actions.…
Inverse game theory is utilized to infer the cost functions of all players based on game outcomes. However, existing inverse game theory methods do not consider the learner as an active participant in the game, which could significantly…
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…
Driven by recent successes in two-player, zero-sum game solving and playing, artificial intelligence work on games has increasingly focused on algorithms that produce equilibrium-based strategies. However, this approach has been less…
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…