[POPLmark] Adequacy for LF

[Kevin Watkins]

Hi all,

I'd like to thank the POPLmark team for their efforts; already with
just one complete solution submitted, I've found the discussion
surrounding it quite interesting.

However, I would like to correct a misconception that is unfortunately
being reinforced by the POPLmark challenge statement: the discussion
of HOAS suggests that it is somehow difficult to calculate
intensionally with variables.  Actually, it's quite easy.  One good
example of the intensional treatment of variable occurrences is the
formal Elf development of the proofs in the report "On the occurrence
of continuation parameters in CPS programs", by Danvy and Pfenning. 
The report is actually also a great illustration of how doing the
machine-checkable representation can lead to better paper proofs, too.
 The formal proofs have been updated for Twelf, and are included in
the standard Twelf distribution, in the examples/cpsocc directory.

Another good set of examples that comes with Twelf is the correctness
of compilation from  Mini-ML to various low-level abstract machines,
in the examples/compile directory.  These analyze HOAS variables
intensionally in order to convert the HOAS into de Bruijn form (which
the low-level machines use).

I realize the team that formulated the challenge couldn't become
experts in all the various approaches summarized there, but it was a
bit disappointing to see this particular misconception reinforced.  In
any case, I'm sure that once someone from the challenge team has a
chance to look at the Twelf examples that do this sort of analysis in
HOAS, the error will be rectified.

Regards,
Kevin Watkins