[Provers] Re: [POPLmark] Submissions page and comments updated

[Peter Sewell]

>Yes, in our work here we use the technical report version as
>definitive; the Milner volume paper was an excerpt written under
>severe space limitations.  The reason to make explicit the control
>stack was to avoid the massive cheat in The Definition of Standard ML
>to do with formalizing exceptions.  There are, officially, many more
>dynamic semantic rules there than meet the eye, whereas in the HS
>formulation there are no such dodges.  This is particularly important
>for mechanization, even as simple a task as simulation, as Gilles Kahn
>discovered way back in the late 80's when he was using Centaur to
>implement The Definition.  Another lesson in the hygienic benefits of
>formalization in a logical framework; pencil and paper let you get
>away with all sorts of sins!

quite :-)


>I have not thought about how best to give semantics to Acute.

I wouldn't suggest anyone should - in this context it's simply an
example of a more intricate dynamic semantics than that of SML, and
one for which the natural pen-and-paper semantics requires computation
under binding contexts.  I would like to know decent formalisation
strategies for those (and they might well vary depending on the choice
of HOAS/De Bruijn/Nominal sets/...)


>The parenthetical remark at the end was an expression of my
>exasperation that we haven't even gotten close in this discussion to
>what I see as the real issues in our solution to the POPLMark
>challenge.  On reflection I realize that it is to the overall good to
>hash out these preliminary matters explicitly, since they are clearly
>not well-understood and since our thinking is at least somewhat at
>odds with yours.

yup.


>The specific issue I mentioned is that when formalizing records, we
>would like to mod out by re-ordering of fields, but there is no good
>way to do this in LF.  The LF methodology provides alpha conversion
>and substitution as structural congruences, but that's it.  You cannot
>impose any other such congruences on terms.  It would be useful to
>explore whether one can relax this a bit and permit more general forms
>of equivalences to be imposed (case in point, re-ordering of record
>fields).  Roberto Virga's work on rewriting for LF goes part of the
>way, but doesn't directly address this problem.  I'd be curious to see
>whether we can build on that to do better.  There is also an issue of
>the "technique" we used to solve the transitivity problem.  The
>argument works, but it feels a bit brittle to me.  Similar issues came
>up in our formalization of the HS semantics in Twelf, requiring even
>dirtier tricks, er I mean more clever techniques, to solve.  I'm not
>at all certain what to think about this.

Maybe it would be useful to change ends for a while - if you have in
your heads a collection of awkward areas and dirty tricks, then simply
enumerating them in a bit more detail would (a) be interesting, and
(b) clarify for the rest of us just where the state-of-the-art
boundary is for Twelf formalisations.

Peter