[TYPES] HOAS versus meta reasoning (Andrew Gacek)

[Marino Miculan]

Andrew Gacek wrote:

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

Also the Theory of Context should be mentioned, which goes back to ten  
years ago. The ToC is an axiomatic theory which allows for structural  
inductive definitions/proofs and recursive definitions over (weak)  
HOAS, within existing systems (we used Coq).

The best references are

An axiomatic approach to metareasoning on systems in higher-order  
abstract syntax
Furio Honsell, Marino Miculan and Ivan Scagnetto
In Proceedings of ICALP'01, Number 2076 in Lecture Notes in Computer  
Science, pages 963-978, 2001

π-calculus in (Co)Inductive Type Theories
Furio Honsell, Marino Miculan and Ivan Scagnetto
Theoretical Computer Science, 253(2), pages 239-285, 2001.

but other papers are available from my web page.

-marino

--
Marino Miculan - Dept Math Compu Sci, University of Udine
miculan at dimi.uniud.it      http://www.dimi.uniud.it/miculan/