The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Brandon Moore wrote:
> > You can find all of these  elements in the implementation that this paper
> > discusses:
> >       http://adam.chlipala.net/papers/ImpurePOPL10/
> > ...and both translation  directions are implemented in Gallina, rather than
> > putting one in Ltac.   The end result is a Gallina term that implements the
> > complete translation from  de Bruijn MiniML to an assembly language, using 
> > PHOAS
> > in some intermediate  languages in a way that does not appear in the final
> > theorem statement (nor in  any need for axioms).
> >      
>
> Thank you for the reference. Unfortunately, I haven't found the reverse
> translation.
> I was hoping to translate from phoas to a type of indexed DeBruijn terms, like
> Source.exp in
> the untyped example. The conversions I see that go onwards from Core.exp are
> translating
> into other phoas types, ultimately flattening into non-indexed data.
>
> I have no idea how to translate back to indexed DeBruijn terms without an
> auxiliary
> well-formedness judgement that basically provides the indices. I suppose if 
> it's
> not in
> ltamer than it's probably not very useful.
>    

Indeed, the closure conversion (file examples/Untyped/CC.v) uses an 
auxiliary well-formedness judgment, but at least it's all implemented in 
Gallina and doesn't need axioms.