Teaching Semantics with a Proof Assistant or No more LSD trip proofs, Tobias Nipkow

Description

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.

Period	24 Jun 2013
Event type	Guest talk
Location	AustriaShow on map