Toward dependent choice: a classical sequent calculus with dependent types

Hugo Herbelin 1, 2 Étienne Miquey 2, 3, *
* Auteur correspondant
2 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 : The dependent sum type of Martin-Löf's type theory provides a strong existential elimination, which allows to prove the full axiom of choice. The proof is simple and constructive: $$AC_A := \lambda H. (\lambda x. wit\,(H\, x), \lambda x. prf\,(H\,x)) : \forall (x:A) \exists (y:B) P(x, y) \Rightarrow \exists (f:A\to B) \forall (x:A) P(x, f (x)) $$ where 'wit' and 'prf' are the first and second projections of a strong existential quantifier. We present here a continuation of Herbelin's works, who proposed a way of scaling up Martin-Löf proof to classical logic. The first idea is to restrict the dependent sum type to a fragment of our system we call N-elimination-free, making it computationally compatible with classical logic. The second idea is to represent a countable universal quantification as an infinite conjunction. This allows to internalize into a formal system (called dPAω) the realizability approach as a direct proof-as-programs interpretation. In a recent paper, Ariola et al. presented a way to construct a CPS-translation for a call-by-need version of the $\bar\lambda\mu\tilde\mu$-calculus, which allows some sharing facilities. Yet, this translation does not enjoy any typing property, and then does not give us a way of proving normalization. Moreover, the $\bar\lambda\mu\tilde\mu$-calculus is typed with sequent calculus [4], which does not allow to manipulate dependent types immediately. We propose to deal with both problems while proving the normalization of our system in two steps. First, we translate our calculus to an adequate version of the $\bar\lambda\mu\tilde\mu$-calculus that allows to manipulate dependent types on the N-elimination-free fragment. Then we will try to adapt the CPS-translation for call-by-need to our case, while adding it a type.
Type de document :
Communication dans un congrès
TYPES 2015, May 2015, Tallinn, Estonia. 2015, 〈〉
Liste complète des métadonnées

Littérature citée [6 références]  Voir  Masquer  Télécharger
Contributeur : Étienne Miquey <>
Soumis le : mercredi 23 décembre 2015 - 12:06:20
Dernière modification le : jeudi 11 janvier 2018 - 06:22:37
Document(s) archivé(s) le : dimanche 30 avril 2017 - 00:45:20


Fichiers produits par l'(les) auteur(s)


  • HAL Id : hal-01247998, version 1




Hugo Herbelin, Étienne Miquey. Toward dependent choice: a classical sequent calculus with dependent types. TYPES 2015, May 2015, Tallinn, Estonia. 2015, 〈〉. 〈hal-01247998〉



Consultations de la notice


Téléchargements de fichiers