Teaching Semantics with a Proof Assistant: No more LSD Trip Proofs
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.
pdf
BibTeX:
@inproceedings{Nipkow-VMCAI12,
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},
publisher=Springer,series=LNCS,volume={7148},pages={24-38},year=2012}