On Fri, 6 Jul 2012 01:42:06 -0400 John Cowan <cowan@mercury.ccil.org>
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.
>

Agreed. (I had somewhat assumed it, in fact.)

Perry
--
Perry E. Metzger		perry@piermont.com

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