9 hours ago, John Cowan wrote:
> Perry E. Metzger scripsit:
>
> > A +1 for switching to an operational semantics. It would be
> > especially cool to develop an executable semantics...
>
> If we are to take the semantics seriously, I think it means
> developing one whose soundness can be established with a proof
> assistant.

Why the hypothetical tone?  There *was* already an implementation of
operational semantics, which *did* use a mechanical tool that can run
them.

--
          ((lambda (x) (x x)) (lambda (x) (x x)))          Eli Barzilay:
                    http://barzilay.org/                   Maze is Life!

_______________________________________________
Scheme-reports mailing list
Scheme-reports@scheme-reports.org
http://lists.scheme-reports.org/cgi-bin/mailman/listinfo/scheme-reports