[Back]


Publications in Scientific Journals:

F. Aschieri:
"Constructive forcing, CPS translations and witness extraction in Interactive realizability";
Mathematical Structures In Computer Science, 27 (2017), 6; 993 - 1031.



English abstract:
In Interactive realizability for second-order Heyting Arithmetic with EM 1 and SK 1 (the excluded middle and Skolem axioms restricted to Σ1 0-formulas), realizers are written in a classical version of Girard's System F. Since the usual reducibility semantics does not apply to such a system, we introduce a constructive forcing/reducibility semantics: though realizers are not computable functionals in the sense of Girard, they can be forced to be computable. We apply this semantics to show how to extract witnesses for realizable Π2 0-formulas. In particular, a constructive and efficient method is introduced. It is based on a new `(state-extending-continuation)-passing-style translation´ whose properties are described with the constructive forcing/reducibility semantics.


"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
http://dx.doi.org/10.1017/S0960129515000468


Created from the Publication Database of the Vienna University of Technology.