Theorem proving support in programming language semantics

We describe several views of the semantics of a simple programming language as formal documents in the calculus of inductive constructions that can be verified by the Coq proof system. Covered aspects are natural semantics, denotational semantics, axiomatic semantics, and abstract interpretation. Descriptions as recursive functions are also provided whenever suitable, thus yielding a a verification condition generator and a static analyser that can be run inside the theorem prover for use in reflective proofs. Extraction of an interpreter from the denotational semantics is also described. All different aspects are formally proved sound with respect to the natural semantics specification.

More work on mechanized metatheory with an eye towards naturalness of representation and automation. This seems to me to relate to Adam Chlipala's work on A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language, which relies on denotational semantics and proof by reflection, in crucial ways. 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 (see also A Very Modal Model of a Modern, Major, General Type System and Verifying Semantic Type Soundness of a Simple Compiler). I find the trend exciting, but of course I also wonder how far we can practically go with it today, given that the overwhelming majority of the literature, including our beloved Types and Programming Languages, is based on A Syntactic Approach to Type Soundness. Even the upcoming How to write your next POPL paper in Coq at POPL '08 centers on the syntactic approach.

Is the syntactic approach barking up the wrong tree, in the long term? The semantic approach? Both? Neither?

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Missing link?


After all that... :-) Thanks for cleaning up after me!

Theorem proving support in programming language semantics

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.