The Coq mailing list

["Flavio L. C. de Moura" <flaviomoura AT unb.br>]

Hi Bruno,

thank you for your answer! I will have a look on it.

Best regards,

Flávio.



Bruno Barras escreveu:
> Flavio L. C. de Moura wrote:
>   
> > Hi there,
> >
> > I am interested on a formalization of the substitution lemma in de
> > Bruijn notation (in Coq). I saw some discussion in coq-club about
> > substitution lemma, but I didn't find nothing in de Bruijn notation
> > anywhere. Does anyone know a formalization of the substitution lemma in
> > de Bruijn notation?
> >     
>
> Hi,
> you did not mention which type system you consider.
> I formalized the metatheory of the Calculus of Constructions (Coq in
> Coq) using de Bruijn indices, so this might be of interest for you. Coq
> sources can be found at:
>   http://www.lix.polytechnique.fr/~barras/CoqInCoq/
> (susbsitution lemma:
> http://www.lix.polytechnique.fr/~barras/CoqInCoq/Types.html#substitution
> ) or as a Coq contribution on coq.inria.fr. There is a paper about this
> formalization on my page and in the contribution.
>
> I don't know much about other type systems, but you can have a look at
> the POPLmark challenge: it is about an extension of system F, and at
> least one participant used de Bruijn indices...
>
> Cheers,
> Bruno Barras.
>
>
>