Interactive Realizability for Second-Order Heyting Arithmetic with EM1 and SK1 - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Pré-Publication, Document De Travail Année : 2012

Interactive Realizability for Second-Order Heyting Arithmetic with EM1 and SK1

Résumé

We introduce a classical realizability semantics based on interactive learning for full second-order Heyting Arithmetic with excluded middle and Skolem axioms over Sigma01-formulas. Realizers are written in a classical version of Girard's System F. Since the usual computability semantics does not apply to such a system, we introduce a constructive forcing/computability semantics: though realizers are not computable functional in the sense of Girard, they can be forced to be computable. We apply these semantics to show how to extract witnesses from realizable Pi02-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/computability semantics.
Fichier principal
Vignette du fichier
RealizersHASEM1final.pdf (564.48 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-00657054 , version 1 (05-01-2012)
hal-00657054 , version 2 (05-03-2012)

Identifiants

  • HAL Id : hal-00657054 , version 2

Citer

Federico Aschieri. Interactive Realizability for Second-Order Heyting Arithmetic with EM1 and SK1. 2012. ⟨hal-00657054v2⟩
114 Consultations
232 Téléchargements

Partager

Gmail Facebook X LinkedIn More