Interactive Proof: Applications to Semantics

Select |




Print


Klein, Gerwin

Klein, Gerwin


2012-04-15


Book Chapter


Software Safety and Security: Tools for Analysis and Verification


85-125


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. The emphasis of the lecture is not on formalising a complex language deeply, but to teach formalisation techniques and proof strategies using simple examples. To this purpose, we cover big- and small step semantics, typing and type safety, as well as a small machine language with compiler and compiler correctness proof.


IOS Press


Isabelle, semantics


NATO Science for Peace and Security Series


978-1-61499-027-7


nicta:5371


Klein, Gerwin. Interactive Proof: Applications to Semantics. In: T. Nipkow, O. Grumberg, B. Hauptmann, G. Kalus Editor, editor/s. Software Safety and Security: Tools for Analysis and Verification. IOS Press; 2012-04-15. 85-125.



Loading citation data...

Citation counts
(Requires subscription to view)