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.
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.
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