The Coq mailing list

[Randy Pollack <rpollack0 AT gmail.com>]

You might be interested in the work by Stephane Lengrand.

Randy



On Fri, Jul 25, 2014 at 5:42 PM, 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