Skip to Main content Skip to Navigation
Conference papers

Toward dependent choice: a classical sequent calculus with dependent types

Hugo Herbelin 1, 2 Étienne Miquey 2, 3, *
* Corresponding author
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [6 references]  Display  Hide  Download

https://hal.inria.fr/hal-01247998
Contributor : Étienne Miquey <>
Submitted on : Wednesday, December 23, 2015 - 12:06:20 PM
Last modification on : Friday, March 27, 2020 - 3:55:51 AM
Long-term archiving on: : Sunday, April 30, 2017 - 12:45:20 AM

File

types2015.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01247998, version 1

Collections

Citation

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

Share

Metrics

Record views

218

Files downloads

165