A Classical Sequent Calculus with Dependent Types

Étienne Miquey 1, 2
1 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 : Dependent types are a key feature of type systems, typically used in the context of both richly-typed programming languages and proof assistants. Control operators, which are connected with classical logic along the proof-as-program correspondence, are known to misbehave in the presence of dependent types, unless dependencies are restricted to values. We place ourselves in the context of the sequent calculus which has the ability to smoothly provide control under the form of the µ operator dual to the common "let" operator, as well as to smoothly support abstract machine and continuation-passing style interpretations. We start from the call-by-value version of the λμμ̃ language and design a minimal language with a value restriction and a type system that includes a list of explicit dependencies and maintains type safety. We then show how to relax the value restriction and introduce delimited continuations to directly prove the consistency by means of a continuation-passing-style translation. Finally, we relate our calculus to a similar system by Lepigre , and present a methodology to transfer properties from this system to our own.
Type de document :
Communication dans un congrès
26th European Symposium on Programming, Apr 2017, Uppsala, Sweden
Liste complète des métadonnées

https://hal.inria.fr/hal-01375977
Contributeur : Étienne Miquey <>
Soumis le : vendredi 20 janvier 2017 - 17:08:26
Dernière modification le : jeudi 15 juin 2017 - 09:09:39
Document(s) archivé(s) le : vendredi 21 avril 2017 - 16:13:50

Fichier

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

Licence


Copyright (Tous droits réservés)

Identifiants

  • HAL Id : hal-01375977, version 3

Collections

INRIA | USPC | PPS

Citation

Étienne Miquey. A Classical Sequent Calculus with Dependent Types . 26th European Symposium on Programming, Apr 2017, Uppsala, Sweden. 〈hal-01375977v3〉

Partager

Métriques

Consultations de
la notice

293

Téléchargements du document

64