Interactive Proof: Applications to Semantics

Select |


Klein, Gerwin

Klein, Gerwin


Book Chapter

Software Safety and Security: Tools for Analysis and Verification


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



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)