The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

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