Lambda the Ultimate

http://arxiv.org/abs/0707.0926

More generally, it seems to reinforce an important trend in using
type-theory-based theorem provers to tackle programming language
design from the semantic point of view ...

I also think that using theorem provers to implement programming
languages is an interesting exercise. The design space is still being
explored. For example, there is a long history in writing down compilers
using the specification language of a sufficiently expressive theorem prover
(e.g. ACL2, HOL, Isabelle/HOL,PVS, Coq, ...) and then using the verification
capabilities of the prover to show correctness of the compiler. These often have a
quite syntactic flavour (lots of operational semantics and commuting
diagram proofs).

The lead paper cited above, and others, take a "semantic" slant. This
can have useful implications, at least when trying to prove properties
of the compiled programs. A variation on this (one I am pursuing
together with colleagues) is to completely avoid having an operational
semantics for the source language; in fact, our source language is a
subset of the logic (classical higher-order logic in our case). If that
sounds arcane, it isn't: the source language is a pure, terminating,
functional programming language which looks quite familiar. It just
doesn't have an execution semantics, but rather uses the builtin
functions of the logic, which have a set-theoretic semantics.
(This is a huge advantage when trying to prove properties of such
functions since operational semantics seems better for meta-theory
than for proof of program properties.)

We are currently working on compilers which translate this language
(which I call TFL, for Total Functional Language) to ARM code,
using a formalized ARM operational semantics due to Anthony Fox,
and a program logic for the ARM due to Magnus Myreen. So I guess
you could say that we use denotational semantics in the front
end, and use axiomatic semantics to connect that to the operational
semantics of the target machine. Similar techniques can be
used to compile to hardware.

Some references if you are interested:

Compilation as Rewriting in Higher Order Logic

Structure of a Proof Producing Compiler for a Subset of Higher-Order Logic

Proof Producing Synthesis of Arithmetic and Cryptographic Hardware

Not only did I neglect to link to the paper when I first posted this, I had not succeeded in finding the related code. But now I have: it's right here, in the Coq contribs directory. Now that I've had a bit more time to look at it, I'm even more impressed: this is Yves Bertot's (coauthor of the Coq'Art book) response to Winskel is (almost) right (PS), which has to be recognized, I think, as a tour de force: the formalization of approximately the first 100 pages of Winskel's The Formal Semantics of Programming Languages: An Introduction.

Winskel's program is to very rapidly introduce the three major approaches to semantic specification of programming languages, namely operational semantics, denotational semantics, and axiomatic semantics; define a very small programming language using all three; and prove that the three semantics so defined are equivalent. "Winskel is (almost) right" formalizes the operational, denotational, and axiomatic semantics in Isabelle/HOL, finding a single, easily-correctable error in the completeness proof for the axiomatic semantics (hence the "almost") and proving the semantics equivalent.

Not to be outdone, Bertot redoes all of this in Coq, adds abstract interpretation to the mix, builds a verification condition generator as well as interpreters to his output, and supports extraction to OCaml code as well as experimenting with the language from within Coq, including, believe it or not, a parser written in Coq. The mind boggles.

It bears mentioning that this development is extremely small in scope: as Bertot says, it ignores issues that it could have treated, e.g. types and compilation. But as a survey of semantic styles and further validation of Winskel's point about the equivalence of operational, denotational, axiomatic, and now abstract interpretation semantics, it seems to hold up quite well, and its fledgling support for end-to-end experimentation within Coq will hopefully inspire others to make their tools more comprehensive and approachable to newcomers.