[TYPES] HOAS versus meta reasoning

[Marcin Zalewski]

Andrei,

I am not an expert and I am not exactly sure what are you looking for
but I think that Parametric HOAS (PHOAS) may be of interest to you:

http://adam.chlipala.net/

There is also a related project, that actually mentions "taming." :) Here it is:

http://ltamer.sourceforge.net/

I hope that you find this reference useful.

Marcin

On Wed, Nov 12, 2008 at 8:26 PM, Andrei Popescu <uuomul at yahoo.com> wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Dear Type Theorists and Practioners,
>
> I would like to know what is the state of the art in taming the interaction between HOAS (higher order abstract syntax) and meta-reasoning/inductive reasoning/recursive definitions.  (I am aware of some of the work, but very probably I am not aware of the latest progress.)
>
> Thank you in advance,
>   Andrei Popescu
>
>
>
>
>
>