[POPLmark] [Provers] Re: Adequacy for LF

[Geoffrey A. Washburn]

On Mon, 9 May 2005, Robert Harper wrote:

> Karl intends to answer this more fully, but, briefly, the difficulty
> with formulating closure conversion in Twelf is not to do with HOAS,
> it's to do with having to get access to the context.  Yes, it is
> difficult to formalize closure conversion in Twelf, but the reason is
> not to do with HOAS.

	I suppose I am confused -- if the difficulty at getting at the
  context is because the context is represented in the meta-language
  via HOAS, doesn't that mean that the reason has to do with HOAS?  Cloud
  you be more specific?  Thanks!

-- 
-- Geoff Washburn | geoffw at cis.upenn.edu | http://www.cis.upenn.edu/~geoffw/ --