Zeitschriftenartikel:
F. Aschieri:
"Constructive Forcing, CPS Translations and Witness Extraction in Interactive Realizability";
Mathematical Structures In Computer Science,
online
(2015),
29.10.2015;
39 S.
Kurzfassung englisch:
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.
"Offizielle" elektronische Version der Publikation (entsprechend ihrem Digital Object Identifier - DOI)
http://dx.doi.org/10.1017/S0960129515000468
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.