## User login## Navigation |
## Theorem proving support in programming language semanticsYves 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, 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. |
## Browse archives## Active forum topics |

## Recent comments

21 hours 15 min ago

1 day 21 hours ago

1 day 22 hours ago

1 day 23 hours ago

3 days 4 hours ago

3 days 5 hours ago

4 days 15 min ago

4 days 1 hour ago

4 days 1 hour ago

4 days 17 hours ago