[TYPES] HOAS versus meta reasoning

[Karl Crary]

The Twelf wiki (twelf.plparty.org) has a lot of material on how to do 
things with higher-order representations.  What specifically are you 
looking to tame? 

    -- Karl Crary


Andrei Popescu 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  
>
>  
>
>
>       
>
>