|
Teaching Semantics with a Proof Assistant or No more LSD trip proofs Abstract: 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. Although the course is still running I will already try to give a preliminary evaluation of the approach.
|