Extending Type Theory with Forcing

Guilhem Jaber 1, 2 Nicolas Tabareau 1, 2 Matthieu Sozeau 3
1 ASCOLA - Aspect and composition languages
LINA - Laboratoire d'Informatique de Nantes Atlantique, Département informatique - EMN, Inria Rennes – Bretagne Atlantique
3 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 : This paper presents an intuitionistic forcing translation for the Calculus of Constructions (CoC), a translation that corresponds to an internalization of the presheaf construction in CoC. Depending on the chosen set of forcing conditions, the resulting type system can be extended with extra logical principles. The translation is proven correct-in the sense that it preserves type checking-and has been implemented in Coq. As a case study, we show how the forcing translation on integers (which corresponds to the internalization of the topos of trees) allows us to define general inductive types in Coq, without the strict positivity condition. Using such general inductive types, we can construct a shallow embedding of the pure \lambda-calculus in Coq, without defining an axiom on the existence of an universal domain. We also build another forcing layer where we prove the negation of the continuum hypothesis.
Type de document :
Communication dans un congrès
LICS 2012 : Logic In Computer Science, Jun 2012, Dubrovnik, Croatia. pp.0-0, 2012
Liste complète des métadonnées

Littérature citée [14 références]  Voir  Masquer  Télécharger

https://hal.archives-ouvertes.fr/hal-00685150
Contributeur : Guilhem Jaber <>
Soumis le : mercredi 4 avril 2012 - 11:49:02
Dernière modification le : mercredi 12 octobre 2016 - 01:23:53
Document(s) archivé(s) le : lundi 26 novembre 2012 - 12:50:36

Fichier

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

Identifiants

  • HAL Id : hal-00685150, version 1

Collections

Citation

Guilhem Jaber, Nicolas Tabareau, Matthieu Sozeau. Extending Type Theory with Forcing. LICS 2012 : Logic In Computer Science, Jun 2012, Dubrovnik, Croatia. pp.0-0, 2012. 〈hal-00685150〉

Partager

Métriques

Consultations de la notice

999

Téléchargements de fichiers

424