[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Scheme-reports] Formal comment: The denotational semantics

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

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

Scheme-reports mailing list