RISC JKU

RISC Talk Announcement

Speaker: Tobias Nipkow, TU München, Germany
Title: Teaching Semantics with a Proof Assistant or No more LSD trip proofs
Date: 24.06. 2013   13:30--14:30
Location: RISC Seminar room
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. At the end of my talk I will give a (predictably positive) evaluation of the approach.
VCAL file: