[POPLmark] [Provers] Re: Adequacy for LF

[Karl Crary]

The problem arises with the use of higher-order assumptions for 
judgements, not for syntax.  (HOAJ, not HOAS, one might say.)  Since 
both of them are usually are win, you usually will see them used 
together.  However, in rare cases such as this where one is a win and 
not the other, there's no reason you can't use just one.  (I've done this.)

    -- Karl


Geoffrey A. Washburn wrote:

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