Teaching Semantics with a Proof Assistant or No more LSD trip proofs
Filed under:
TALK
Prof. Tobias Nipkow (TU Munich, Germany), 24 June 2013, 1:30 p.m., RISC seminar room castle
| When |
Jun 24, 2013
from 01:30 PM to 03:00 PM |
|---|---|
| Where | RISC seminar room castle |
| Add event to calendar |
vCal
iCal
|
Teaching Semantics with a Proof Assistant or No more LSD trip proofs
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.