Personal tools
You are here: Home / Internal / RISC Forum / 2013 / Risc Colloquium

Risc Colloquium

Prof. Tobias Nipkow (TU Muenchen): Teaching Semantics with a Proof Assistant
When Jun 24, 2013
from 01:30 PM to 02:30 PM
Where Seminar Room
Add event to calendar vCal
iCal

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.

« August 2025 »
August
MoTuWeThFrSaSu
123
45678910
11121314151617
18192021222324
25262728293031
Upcoming Events
RISC Forum Oct 06, 2025 01:30 PM - 01:45 PM — RISC
RISC Forum Oct 06, 2025 01:30 PM - 02:30 PM — RISC
RISC Forum Oct 13, 2025 01:30 PM - 01:45 PM — RISC
RISC Forum Oct 20, 2025 01:30 PM - 01:45 PM — RISC
RISC Forum Oct 27, 2025 01:30 PM - 01:45 PM — RISC
Previous events…
Upcoming events…