A Classical Sequent Calculus with Dependent Types

Étienne Miquey 1
1 GALLINETTE - Gallinette : vers une nouvelle génération d'assistant à la preuve
Inria Rennes – Bretagne Atlantique , LS2N - Laboratoire des Sciences du Numérique de Nantes
Abstract : Dependent types are a key feature of the proof assistants based on the Curry-Howard isomorphism. It is well-known that this correspondence can be extended to classical logic by enriching the language of proofs with control operators. However, they are known to misbehave in the presence of dependent types, unless dependencies are restricted to values. Moreover, while sequent calculi are naturally tailored to smoothly support 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 λµ̃µ-calculus. We design a minimal language with a value restriction and a type system that includes a list of explicit dependencies to 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.
Document type :
Journal articles
Complete list of metadatas

Cited literature [49 references]  Display  Hide  Download

https://hal.inria.fr/hal-01519929
Contributor : Étienne Miquey <>
Submitted on : Saturday, December 15, 2018 - 1:16:22 AM
Last modification on : Tuesday, March 26, 2019 - 9:25:22 AM
Long-term archiving on : Saturday, March 16, 2019 - 12:20:16 PM

File

dLtp.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01519929, version 3

Citation

Étienne Miquey. A Classical Sequent Calculus with Dependent Types. ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, In press, pp.1-48. ⟨hal-01519929v3⟩

Share

Metrics

Record views

164

Files downloads

338