Failure is Not an Option An Exceptional Type Theory

Pierre-Marie Pédrot 1 Nicolas Tabareau 2
2 GALLINETTE - GALLINETTE
Inria Rennes – Bretagne Atlantique , LS2N - Laboratoire des Sciences du Numérique de Nantes
Abstract : We define the exceptional translation, a syntactic translation of the Calculus of Inductive Constructions (CIC) into itself, that covers full dependent elimination. The new resulting type theory features call-by-name exceptions with decidable type-checking and canonicity, but at the price of inconsistency. Then, noticing parametricity amounts to Kreisel's realizability in this setting, we provide an additional layer on top of the exceptional translation in order to tame exceptions and ensure that all exceptions used locally are caught, leading to the parametric exceptional translation which fully preserves consistency. This way, we can consistently extend the logical expressivity of CIC with independence of premises, Markov's rule, and the negation of function extensionality while retaining η-expansion. As a byproduct, we also show that Markov's principle is not provable in CIC. Both translations have been implemented in a Coq plugin, which we use to formalize the examples.
Type de document :
Communication dans un congrès
ESOP 2018 - 27th European Symposium on Programming, Apr 2018, Thessaloniki, Greece. Springer, 10801, pp.245-271, LNCS. 〈10.1007/978-3-319-89884-1_9〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01840643
Contributeur : Nicolas Tabareau <>
Soumis le : lundi 16 juillet 2018 - 15:30:59
Dernière modification le : vendredi 5 octobre 2018 - 15:21:49
Document(s) archivé(s) le : mercredi 17 octobre 2018 - 15:52:29

Fichier

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

Identifiants

Collections

Citation

Pierre-Marie Pédrot, Nicolas Tabareau. Failure is Not an Option An Exceptional Type Theory. ESOP 2018 - 27th European Symposium on Programming, Apr 2018, Thessaloniki, Greece. Springer, 10801, pp.245-271, LNCS. 〈10.1007/978-3-319-89884-1_9〉. 〈hal-01840643〉

Partager

Métriques

Consultations de la notice

414

Téléchargements de fichiers

57