[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