The Definitional Side of the Forcing

Guilhem Jaber 1 Gabriel Lewertowski 2, 1 Pierre-Marie Pédrot 2 Matthieu Sozeau 3, 1 Nicolas Tabareau 2
2 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, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique, Inria de Paris
Abstract : This paper studies forcing translations of proofs in dependent type theory, through the Curry-Howard correspondence. Based on a call-by-push-value decomposition, we synthesize two simply-typed translations: i) one call-by-value, corresponding to the translation derived from the presheaf construction as studied in a previous paper ; ii) one call-by-name, whose intuitions already appear in Kriv-ine and Miquel's work. Focusing on the call-by-name translation, we adapt it to the dependent case and prove that it is compatible with the definitional equality of our system, thus avoiding coherence problems. This allows us to use any category as forcing conditions , which is out of reach with the call-by-value translation. Our construction also exploits the notion of storage operators in order to interpret dependent elimination for inductive types. This is a novel example of a dependent theory with side-effects, clarifying how dependent elimination for inductive types must be restricted in a non-pure setting. Being implemented as a Coq plugin, this work gives the possibility to formalize easily consistency results, for instance the consistency of the negation of Voevodsky's univalence axiom.
Type de document :
Communication dans un congrès
Logics in Computer Science, May 2016, New York, United States. 〈10.1145/http://dx.doi.org/10.1145/2933575.2935320〉
Liste complète des métadonnées

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

https://hal.archives-ouvertes.fr/hal-01319066
Contributeur : Gabriel Lewertowski <>
Soumis le : vendredi 20 mai 2016 - 12:02:37
Dernière modification le : samedi 25 février 2017 - 01:02:24

Fichier

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

Identifiants

Collections

Citation

Guilhem Jaber, Gabriel Lewertowski, Pierre-Marie Pédrot, Matthieu Sozeau, Nicolas Tabareau. The Definitional Side of the Forcing. Logics in Computer Science, May 2016, New York, United States. 〈10.1145/http://dx.doi.org/10.1145/2933575.2935320〉. 〈hal-01319066〉

Partager

Métriques

Consultations de
la notice

584

Téléchargements du document

178