[TYPES] HOAS versus meta reasoning

[murdoch gabbay]

Dear Alexander,

In a recent paper Martin Hofmann and I make the weak HOAS-syle datatype
   mu X. (Var -> X) + (X x X) + Var
compatible with a flavour of nominal techniques:
   http://www.gabbay.org.uk/papers.html#nomrs
(In a final note we hypothesise how similar techniques might be
applicable to model abstraction in strong HOAS "(X -> X)" style.)

I've written a survey and update paper on nominal techniques, which is
now under consideration for publication.
   http://www.gabbay.org.uk/papers.html#setfnt
Comments are welcome.

Jamie


-- 
Murdoch James Gabbay
www.gabbay.org.uk

--- Which is worse, ignorance or apathy?
--- Who knows?  Who cares?