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

[Peter Sewell]

Perhaps it would be useful to clarify our original thinking
w.r.t. evaluation contexts in the challenge problems. 

We would like to understand the best tools and idioms to use for
expressing the definitions and metatheory of programming languages.
Now, we're really concerned

1) with expressing the _primary_ definition of a
   language, especially while it is under development, rather than
   with _encoding_ an existing pen-and-paper definition; and

2) with non-trivial languages, e.g. including exceptions, new name
   generation, computation under certain binders, and concurrency,
   and with an eye towards definitions in the 100-page scale.

These affect the representation trade-offs: if your focus is language
design, especially for a large language, you need the primary
definition to be concise, easy to understand, and easy to change.  On
the other hand, if your focus is metatheory proofs about an existing
language definition, you may care most about making those proofs
slick.

In posing the challenge we had to simplify in both directions: to make
it possible to compare the results we fixed a particular pen-and-paper
definition, and to make the challenge manageable we cut down to a
small calculus.

For that calculus in isolation, whether one uses explicit reduction
closure rules or evaluation contexts makes little difference to an
informal development.  The definitions are equally comprehensible; the
proofs are slightly simpler for the former style.  It wouldn't be
surprising to find that mechanisation is smoother in the former style.

As one moves to the world of (1) and (2), however, we believe that for
pen-and-paper semantics using evaluation contexts is an important
pragmatic tool for writing concise and malleable definitions.  We
therefore guess that a good mechanized definition style would also use
evaluation contexts here, and so we want to see how it would be done
in the various systems.  Being able to contrast the different possible
evaluation context formalisations, including e.g. Frank's dependent
functions, would be very interesting.

(Of course, it's possible that we're wrong about this: formalisation
might shift the balance back towards preferring explicit rules for
reduction closure, exception propagation, global name extrusion, etc.
If so, we'd obviously like to know it -- but it needs an argument that
applies to (2), not just to Fsub.)

The bottom line is that we're not really asking how best to formalise
Fsub, but how best to express some new (and large) semantics in the
future.

Peter