[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Scheme-reports] Formal comment: The denotational semantics
- To: "Perry E. Metzger" <perry@x>
- Subject: Re: [Scheme-reports] Formal comment: The denotational semantics
- From: John Cowan <cowan@x>
- Date: Fri, 6 Jul 2012 01:42:06 -0400
- Cc: Michael Sperber <sperber@x>, scheme-reports@x
- In-reply-to: <20120705220148.37a1a2b0@jabberwock.local>
- References: <y9ltxxn2vv9.fsf@deinprogramm.de> <CAMMPzYMb=e9iHiJhcM5QXv=wFENK=2+9nytvMSOBsfnhBe=6GA@mail.gmail.com> <20120705220148.37a1a2b0@jabberwock.local>
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.
--
John Cowan cowan@x http://www.ccil.org/~cowan
Dievas dave dantis; Dievas duos duonos --Lithuanian proverb
Deus dedit dentes; deus dabit panem --Latin version thereof
Deity donated dentition;
deity'll donate doughnuts --English version by Muke Tever
God gave gums; God'll give granary --Version by Mat McVeagh
_______________________________________________
Scheme-reports mailing list
Scheme-reports@x
http://lists.scheme-reports.org/cgi-bin/mailman/listinfo/scheme-reports