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

[Robert Harper]

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.

Bob

On May 2, 2005, at 10:49 PM, Stephan Zdancewic wrote:

> Robert Harper wrote:
>
>> Please see the Harper-Stone Definition of Standard ML, in particular 
>> the dynamic semantics of the internal language.  Whether formally or 
>> informally, there is no room or use for evaluation contexts as a 
>> means of specifying the operational semantics.
>
> 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?
>
>> To repeat, there is absolutely no obstacle to using this method for 
>> the challenge, but there is no advantage to it of any kind.  Our 
>> formulation is adequate for the task, and we have demonstrated that 
>> it is entirely suitable for solving the challenge problem.  It is not 
>> a good use of our time, and there is nothing to be learned, from 
>> trying to redo it in some style that is presumed a priori to be 
>> better.
>
> Perhaps one useful by-product of this conversation might be a clear 
> articulation *why* evaluation contexts aren't useful for formal 
> methods. I have found them useful in my own work, and so have many 
> others. Do you have a good explanation why SOS is better?  This would 
> allow others (like me) who are trying to formalize their own research 
> to draw on your experiences and perhaps avoid some pitfalls.
> Thanks,
>  Steve
>
> _______________________________________________
> Poplmark mailing list
> Poplmark at lists.seas.upenn.edu
> http://lists.seas.upenn.edu/mailman/listinfo/poplmark