Home

Theorem proving support in programming language semantics

Yves Bertot, one of the coauthors of the Coq'Art book, has made available a tech report on Theorem proving support in programming language semantics, which describes how Coq can be used to support an exhasutive "views" approach to program semantics, using a toy imperative language from Glyn Winskel's book, The Formal Semantics of Programming Languages, and specifying a family of kinds of semantics on it, following Winskel's treatment.

Bertot follows the work of Tobias Nipkow, in Winskel is (almost) Right: Towards a Mechanized Semantics Textbook using Isabelle, but he shows how Coq's support for reflection allows this treatment to be carried out in a lean, condensed manner. The 23 page paper covers Plotkin-style SOS semantics, Kahn's natural semantics, Dijkstra's weakest precondition semantics, a simple CPO denotational semantics that I assume is due to Winskel & finally uses the denotational model as a basis for abstract interpretation.

By Charles Stewart at 2007-07-09 15:22 | Semantics | other blogs | 7970 reads

Comment viewing options

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

Very neat!

Very neat!

By Ehud Lamm at Tue, 2007-07-10 10:34 | login or register to post comments

Very neat indeed!

He gave this as a 1-week summer course. It was indeed very interesting, and Yves is a good teacher, too. Unfortunately, to me this course's usefulness was limited by my missing Coq practice. He gave out his proof scripts and slides, so if you ask kindly, he might send you the former. I doubt he will give out the slides, though -- his lectures contained the phrase "This slide is wrong, ..." pretty often. ;)
It didn't hurt the lecture, since it were all small typos, like wrong or missing indexes, as happens if you have to edit program output to fit onto a slide. But it would probably be very distracting if one were to read the slides offline (and fixing it would presumably require quite some effort). The proof scripts are of course correct!

By Thomas Schilling at Fri, 2007-08-03 22:27 | login or register to post comments