A sequent calculus with dependent types for classical arithmetic

Étienne Miquey 1
1 GALLINETTE - GALLINETTE
Inria Rennes – Bretagne Atlantique , LS2N - Laboratoire des Sciences du Numérique de Nantes
Abstract : In a recent paper, Herbelin developed a calculus dPAω in which constructive proofs for the axioms of countable and dependent choices could be derived via the encoding of a proof of countable universal quantification as a stream of it components. However, the property of normalization (and therefore the one of soundness) was only conjectured. The difficulty for the proof of normalization is due to the simultaneous presence of dependent dependent types (for the constructive part of the choice), of control operators (for classical logic), of coinductive objects (to encode functions of type N → A into streams (a₀, a₁, ...)) and of lazy evaluation with sharing (for these coinductive objects).Building on previous works, we introduce in this paper a variant of dPAω presented as a sequent calculus. On the one hand, we take advantage of a variant of Krivine classical realizability we developed to prove the normalization of classical call-by-need. On the other hand, we benefit of dL, a classical sequent calculus with dependent types in which type safety is ensured using delimited continuations together with a syntactic restriction. By combining the techniques developed in these papers, we manage to define a realizability interpretation à la Krivine of our calculus that allows us to prove normalization and soundness.
Type de document :
Communication dans un congrès
LICS 2018 - 33th Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2018, Oxford, United Kingdom. pp.1-22
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01703526
Contributeur : Étienne Miquey <>
Soumis le : mercredi 23 mai 2018 - 18:16:02
Dernière modification le : mercredi 6 juin 2018 - 09:50:20

Fichiers

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

Identifiants

  • HAL Id : hal-01703526, version 2
  • ARXIV : 1805.09542

Collections

Citation

Étienne Miquey. A sequent calculus with dependent types for classical arithmetic. LICS 2018 - 33th Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2018, Oxford, United Kingdom. pp.1-22. 〈hal-01703526v2〉

Partager

Métriques

Consultations de la notice

112

Téléchargements de fichiers

40