7 citations · 7 across the 4 of their papers we have counts for
4 papers
A Monadic Framework for Interactive Realizability
Giovanni Birolo
We give a new presentation of interactive realizability with a more explicit syntax. Interactive realizability is a realizability semantics that extends the Curry-Howard correspond…
Interpreting a Classical Geometric Proof with Interactive Realizability
Giovanni Birolo
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 realizabili…
A Witness Extraction Technique by Proof Normalization Based on Interactive Realizability
Giovanni Birolo
We present a new set of reductions for derivations in natural deduction that can extract witnesses from closed derivations of simply existential formulas in Heyting Arithmetic (HA)…
Interactive Realizability, Monads and Witness Extraction
Giovanni Birolo
In this dissertation we collect some results about "interactive realizability", a realizability semantics that extends the Brouwer-Heyting-Kolmogorov interpretation to (sub-)classi…