[TYPES] HOAS versus meta reasoning

[Andrei Popescu]

Dear Andrew and Karl, 

I thank you very much for your comments and references.  

To answer Karl's question, I used the word "taming" because, as far as I see, the interaction between meta-reasoning (by which I understand reasoning about the object system) and HOAS is a wild issue.  Going back one level and (case-)analyzing the meta-logic inference itself in a meta-meta logic seems like an elegant, but extreme measure to take  -- for one thing, it breaks the ties with more conventional frameworks for developing mathematics, such as the ones of Coq, Isabelle/HOL or PVS, where a working mathematician feels immediately comfortable (thanks to the standard foundations), and where many libraries of theories are available. Staying in a conventional framework, on the other hand, requires compromises on the hassle-free (i.e., typing-context-free, substitution-free, bound-variables-free etc.) aspect of the representation.  I was not looking for taming any aspect in particular, 
but for getting a picture of the recent progress within the above approaches and maybe others in between.  

Regards, 
 Andrei Popescu  


--- On Thu, 11/13/08, Karl Crary <crary at cs.cmu.edu> wrote:

> From: Karl Crary <crary at cs.cmu.edu>
> Subject: Re: [TYPES] HOAS versus meta reasoning
> To: uuomul at yahoo.com
> Cc: types-list at lists.seas.upenn.edu
> Date: Thursday, November 13, 2008, 12:43 AM
> 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  
> >  
> > 
> >       
> >