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

[Peter Sewell]

Stephan Zdancewic wrote:
>I'm not sure I understand what you intend here.  According to the paper  
>"A Type-Theoretic Interpretation of Standard ML" (Chris Stone and Robert 
>Harper, Milner Festschrifft. 2000), figure 6 on page 8, the operational 
>semantics *are* described using evaluation contexts.  Was that 
>formalization unnecessarily complicated by their use?


Robert Harper wrote:
>We used control stacks explicitly, not evaluation contexts (with 
>filling and all that rot).
>
>The reason why is that when you do the metatheory (by hand or 
>otherwise) you have to reproduce what the SOS formulation would've 
>given you straight away.


Looking at the techreport (CMU-CS-97-147, p30ff) there's a different
presentation from the Festschrifft, with the same grammar of atomic
evaluation contexts but with some 35 administrative reduction rules to
push them on and off an explicit frame stack.

For me personally, that seems notationally heavy - I'd be prepared to
have slightly more complex metatheory proofs in order to get rid of
those rules.  I wouldn't argue that that isn't a matter of taste,
though - certainly it isn't fundamental.

A more interesting question is how to best express computation under
_binding_ contexts, eg under pi-calculus-like new binders, or for
semantics using instantiation under value-let bindings rather than
substitution.  If you were formalising that, would you still do so
in the same style, with the administrative rules changing the binding
structure??

(We had a lot of this kind of thing in our Acute semantics, with
concurrency and with computation under module definitions; it seemed
necessary to use several different flavours of binding evaluation
context to express it concisely.)



Robert Harper wrote:
>working on real issues in logical frameworks (such as how to 
>incorporate more interesting structural congruences, a point where a 
>*legitimate* criticism of our solution can be levelled.)

meaning?

Peter