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

[Stephan Zdancewic]

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