# 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