Interactive Proof: Applications to Semantics
Klein Gerwin · NATO science for peace and security series. D, Information and communication security · 2012
Building on a previous lecture in the summer school, the introduction to interactive proof, this lecture demonstrates a specific application of interactive proof assistants: the semantics of programming languages. In particular, I show how to formalise a small imperative programming language in the theorem prover Isabelle/HOL, how to define its semantics in different variations, and how to prove properties about the language in the theorem prover.