[POPLmark] Lists of binders in HOAS

Benjamin Pierce bcpierce at cis.upenn.edu
Mon May 9 16:23:48 EDT 2005


> My attention has been drawn to the following statement on page 6 of the 
> Poplmark challenge: "However, our experience also suggests that it is 
> often difficult to use HOAS to represent many problems.  For example, 
> there are many languages with constructs that require lists of binders 
> that do not have any obvious encoding into HOAS."
>
> ...
> 
> As far as I know, this technique is quite robust.  So I'm curious, what 
> did the challenge authors have in mind?

We were unaware of this technique until seeing the Twelf solution to the
challenge.  The sentence is being removed from the next revisision of the
challenge.

Regards,

    - Benjamin



More information about the Poplmark mailing list