Teaching Semantics with a Proof Assistant: No more LSD Trip Proofs

Tobias Nipkow

We describe a course on the semantics of a simple imperative programming language and on applications to compilers, type systems, static analyses and Hoare logic. The course is entirely based on the proof assistant Isabelle and includes a compact introduction to Isabelle. The overall aim is to teach the students how to write correct and readable proofs.



author={Tobias Nipkow},
title={Teaching Semantics with a Proof Assistant: No more {LSD} Trip Proofs},
booktitle={Verification, Model Checking, and Abstract Interpretation (VMCAI 2012)},
editor={V. Kuncak and A. Rybalchenko},