Publications in Scientific Journals:
F. Aschieri:
"Constructive Forcing, CPS Translations and Witness Extraction in Interactive Realizability";
Mathematical Structures In Computer Science,
online
(2015),
29.10.2015;
39 pages.
English abstract:
In Interactive realizability for second-order Heyting Arithmetic with EM1 and SK1 (the excluded middle and Skolem axioms restricted to Σ10-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 Π20-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.