After the course students can:
- develop a formalization in a proof assistant
- implement a simple proof assistant
- select an appropriate proof assistant for a given purpose
- install and use a proof assistant that they have not seen before
|
|
|
This course is an introduction to the field of proof assistants, also known as proof checkers or interactive theorem provers. These are implementations of logical systems, programs for the development and verification of formal proofs, both for mathematics and for computer science. The course presents the current state of the art in proof assistants, and then teaches two specific proof assistants in detail.
The first of these is the Isabelle system. With this proof assistant we focus on the user perspective, and will develop a non-trivial proof in full detail. The second is the HOL system. With this system we focus on the implementation architecture and automation of the system. Finally an overview of the main current proof assistants is presented, and some of the large efforts in this area that are currently ongoing are reviewed.
Proof assistants, both for mathematics and for computer science, are one of the research topics of the Foundations group.
Instructional Modes
- Lecture
- Presentation
- Self-study
|
 |
|
|
|
Predicate logic. Lambda calculus. Functional programming.
|
|
| The final note will be the average of three marks:
the mark for the Isabelle formalization
the mark for the small LCF-style proof assistant
the mark for the presentation in the third part of the course |
|
|