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 the type systems used by the proof assistants based on the intuitionistic Curry-Howard correspondence. On the other hand, this correspondence can be extended to classical logic provided the language of proofs is enriched with control operators. Alas, control operators are known to misbehave in the presence of dependent types, unless dependencies are restricted to values. Besides, while sequent calculi smoothly support abstract machine and continuation-passing style interpretations, there is no such presentation of a language with dependent types. The main achievement of this paper is to give a sequent calculus presentation of a call-by-value language with a control operator and dependent types, and to justify its soundness through a continuation-passing style translation. 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 :
Pré-publication, Document de travail
2017
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01519929
Contributeur : Étienne Miquey <>
Soumis le : mardi 9 mai 2017 - 15:36:55
Dernière modification le : jeudi 15 juin 2017 - 09:09:39
Document(s) archivé(s) le : jeudi 10 août 2017 - 13:34:24

Fichier

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

Identifiants

  • HAL Id : hal-01519929, version 1

Collections

INRIA | USPC | PPS

Citation

Étienne Miquey. A Classical Sequent Calculus with Dependent Types. 2017. 〈hal-01519929〉

Partager

Métriques

Consultations de
la notice

124

Téléchargements du document

51