The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

It depends on what you mean by sequent calculus. If a natural deduction is all right for your purposes, then Hugo Herbelin and I worked out most of the details in [ http://drops.dagstuhl.de/opus/volltexte/2014/4631/pdf/10.pdf ]. The guard condition is left undefined though. There is some ongoing work to make it precise, but in this work, we just assumed it existed.

If you need a sequent calculus with right and left introduction rules. Then this is still poorly understood mostly because of dependent elimination. Hugo Herblin's habilitation (in French) has a one page remark on how this could be achieved [ http://pauillac.inria.fr/~herbelin/habilitation/memoire.ps ] but it is quite preliminary.

On 25 July 2014 23:42, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

Is there a presentation of all the typehood rules of Coq

as a sequent calculus such that the

 coq's typechecker accepts that a term t has type T iff

there is a a derivation of the judgement t:T in the above calculus?

We're mainly concerned about a core fragment Coq which

includes Pi types, a cumulative hierarchy of universes and inductive types/match construct.

We're asking because if this collection of rules is not huge, we

might be interested in adapting the proofs in [1] to prove

the consistency of these rules.

[1] : Abhishek Anand, and Vincent Rahli. Towards a Formally Verified Proof Assistant. ITP 2014

Regards,

 Abhishek and Vincent