The Coq mailing list

[Kenneth Adam Miller <kennethadammiller AT gmail.com>]

Wow!

Thank you so much to all of you.

On May 31, 2016 1:26 PM, "Xavier Leroy" <Xavier.Leroy AT inria.fr> wrote:

On 31/05/16 07:20, Kenneth Adam Miller wrote:
> I've read seven chapters into Interactive Theorem Proving and
> Program Development, and I don't think either axiomatic or
> operational semantics are mentioned anywhere

Just hold tight for a few more chapters!  The chapters Imp, Equiv,
Hoare, Hoare2 and Smallstep explain very well the approach already
mentioned in this thread, namely defining the syntax and (operational or
axiomatic) semantics of a programming language in Coq, and proving
properties about them.

> You can't add a semantics for a language built under and by Coq?

You can certainly define semantics for a programming language in Coq.

> What about Mezzo, there is a language that was built with Coq.

Not really "built with Coq".  Rather, its abstract syntax, operational
semantics and type systems were formalized using Coq, then proved sound.

> If you're right, then I guess that the mezzo source files just map
> down to Coq types eventually.

You could look up the terms "shallow embedding" and "deep embedding"
in the literature.  What you have in mind sounds like a deep embedding
but the Mezzo formalization, and many other P.L. formalizations in
Coq, use the "shallow embedding" approach.

Hope this helps,

- Xavier Leroy