Teaching Semantics with a Proof Assistant or No more LSD trip proofs
Speaker: Tobias Nipkow
Date: 24/06/2013
Time: 13:30 - 14:30
Time: 13:30 - 14:30
Location: RISC Seminar room
The gulf between many computer science students and rigorous proofs is well known and much lamented. Teachers are frequently confronted with student ``proofs'' that look more like LSD trips than coherent chains of logic. In this talk I will present a new Programming Language Semantics course that bridges the gulf with the help of a proof assistant, Isabelle. During the first quarter of the semester the students are introduced to machine-checked proofs. The rest of the course covers a wide spectrum of topics centered around a simple imperative language: operational semantics, compilation, types, program analysis and Hoare logic. At the end of my talk I will give a (predictably positive) evaluation of the approach.