coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: RE : Re: [Coq-Club]Type system in Coq

From: Frederic Blanqui <blanqui AT loria.fr>
To: Fabrice Lemercier <nouvid-coq AT yahoo.fr>
Cc: Lionel Elie Mamane <lionel AT mamane.lu>, coq-club AT pauillac.inria.fr
Subject: Re: RE : Re: [Coq-Club]Type system in Coq
Date: Thu, 8 Jun 2006 17:48:28 +0200 (CEST)
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

you can perhaps find some help by looking at CoLoR, the Coq library on rewriting and termination at http://color.loria.fr/, in Adam Koprowski's formalization of simply-typed lambda-calculus. see in particular the file TermsTyping.

[Coq-Club]Type system in Coq, Fabrice Lemercier
- Re: [Coq-Club]Type system in Coq, Santiago Zanella B�guelin
- Re: [Coq-Club]Type system in Coq, Lionel Elie Mamane
  - RE : Re: [Coq-Club]Type system in Coq, Fabrice Lemercier
    - Re: RE : Re: [Coq-Club]Type system in Coq, Roland Zumkeller
    - Re: RE : Re: [Coq-Club]Type system in Coq, Lionel Elie Mamane
    - Re: RE : Re: [Coq-Club]Type system in Coq, Frederic Blanqui