coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
- To: Coq Club <coq-club AT inria.fr>
- Cc: "coqdev AT inria.fr" <coqdev AT inria.fr>
- Subject: Re: [Coq-Club] Coq's typehood rules as a sequent calculus?
- Date: Mon, 28 Jul 2014 11:21:30 +0200
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.
Sorry: it's page 74.
- [Coq-Club] Coq's typehood rules as a sequent calculus?, Abhishek Anand, 07/25/2014
- Re: [Coq-Club] Coq's typehood rules as a sequent calculus?, Arnaud Spiwack, 07/28/2014
- Re: [Coq-Club] Coq's typehood rules as a sequent calculus?, Arnaud Spiwack, 07/28/2014
- Re: [Coq-Club] Coq's typehood rules as a sequent calculus?, Randy Pollack, 07/28/2014
- Re: [Coq-Club] Coq's typehood rules as a sequent calculus?, Arnaud Spiwack, 07/28/2014
Archive powered by MHonArc 2.6.18.