Interactive Learning Based Realizability and 1-Backtracking Games

We prove that interactive learning based classical realizability (introduced by Aschieri and Berardi for first order arithmetic) is sound with respect to Coquand game semantics. In particular, any realizer of an implication-and-negation-free arithmetical formula embodies a winning recursive strategy...

Descrición completa

Detalles Bibliográficos
Autor Principal: Federico Aschieri
Formato: Artigo
Idioma:English
Publicado: Open Publishing Association 2011-01-01
Series:Electronic Proceedings in Theoretical Computer Science
Acceso en liña:http://arxiv.org/pdf/1101.5441v1