[POPLmark] An unscientific comparison

[James Cheney]

Hi,

As a result of discussions on this list I saw one way to deal with the
inequality judgments in Hannan's closure conversion system.  Yesterday
and this morning I attempted to implement Hannan's paper's first
definition of closure conversion in LF (Twelf) and alpha Prolog. 
(I have not attempted to prove anything about the LF versions using
Twelf; but both versions appear to do what Hannan's paper versions say.)
Rather than spam people who may not be interested with huge amounts of
code and details, I placed the developments on my web page.  Anyone
interested may take a look at:

http://homepages.inf.ed.ac.uk/jcheney/cconv/

My results for both versions are mixed.  While I am now certain that the
judgments *can* be encoded in LF (just as Karl Crary and others have
asserted), my encodings do not appear to support the hypothesis that
Hannan's rules can be directly (and correctly) mapped into "elegant"
LF.  However, absence of evidence is not evidence of absence:  I am not
attempting to draw any conclusions from this, especially since I have
not heard back from John Hannan and it is possible that my LF encodings
are completely different from what he did.  My aim is solely to add some
raw data to the discussion as to what various formalisms can do and how.

Suggestions as to how to improve either encoding are welcome.

--James
-- 
James Cheney <jcheney at inf.ed.ac.uk>