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

• Type: Journal
• Year: 2012
• Where: VMCAI
• Authors: Tobias Nipkow
• Keywords: Hoare Logic, Imperative Programming Language, Software Engineering, Static Analyses, VMCAI 2012