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

Federico Aschieri 1
1 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
Abstract : 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.
Type de document :
Pré-publication, Document de travail
2012
Liste complète des métadonnées

https://hal.inria.fr/hal-00657054
Contributeur : Federico Aschieri <>
Soumis le : lundi 5 mars 2012 - 22:02:08
Dernière modification le : mardi 17 avril 2018 - 11:30:34
Document(s) archivé(s) le : mercredi 6 juin 2012 - 02:32:11

Fichiers

RealizersHASEM1final.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00657054, version 2

Collections

INRIA | PPS | USPC

Citation

Federico Aschieri. Interactive Realizability for Second-Order Heyting Arithmetic with EM1 and SK1. 2012. 〈hal-00657054v2〉

Partager

Métriques

Consultations de la notice

215

Téléchargements de fichiers

132