[Zurück]


Zeitschriftenartikel:

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



Kurzfassung englisch:
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.


"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.