Interactive Theorem Proving

Course Informations

In a type-theoretic setting programs can be understood as well-typed computable functions between
appropriate types and systems are functions defined on process types. Due to the Curry-Howard-Iso-
morphism it is possible to extract a program from a proof of a corresponding theorem. This can be
done also for systems.

New theorem provers combine program and system specification and verification tools and can also
be used as a prototype interpreter, as it is with functional programming languages. The lectures shall
give an intentional introduction to these approaches using the concepts of higher-order logic, recursive
and corecursive functions and some applications.

This lecture on Interactive Theorem Proving in Winter term 2010/11 combines several different aspects.
First, it introduces into some theoretical foundations for the construction and use of theorem provers as
reasoning tools. A second topic in this lecture is dedicated to some methods in specification, verification
and proof theory. And finally, using interesting and challenging applications the students are made acquainted
with the proof systems PVS, Isabelle, and Maude in the tutorials/practicals.

Lecturer:

Dr. Michael Posegga

Actual Informations to the beginning, time table etc.

The lectures take place in room INF/E05 on Tuesday, 5th DS (14:50 - 16:20) and on Wednesday, 2ndd DS
(09:20 - 10:50). They begin in the first week on Tuesday, 12 October.

The tutorial/practical takes place in room 3027 on Tuesday, 3rd DS (11:10 - 12:40) and begins in
the second week on Tuesday, 19 October.

Teaching Material

Here you can find the script and the tutorial sheets for the lecture "Interactive Theorem Proving" for the
Winter term 2010/2011.

Here are the tutorial sheets:

Michael Posegga