[TYPES] HOAS versus meta reasoning

[Adam Poswolsky]

Hi Andrei,

I would like to draw your attention to Delphin which tackles reasoning 
over higher-order encodings using a functional paradigm.  The system is 
available for download and a quick user manual is available in my 
dissertation.

http://cs-www.cs.yale.edu/homes/delphin/delphin.htm

--Adam


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