Interactive Proof Assistants (IPA)
Course content
Interactive theorem proving is concerned with carrying out machine-checked proofs and developing the systems that check these proofs—proof assistants. Proof assistants, like Coq, Lean, and Isabelle, are used today to build highly critical systems and verify deep mathematical results. Landmark achievements in this area include formally verified compilers, operating system kernels, and distributed systems, as well as formal proofs of deep mathematical results, such as the four-colour, the Feit–Thompson, and Gödel's incompleteness theorems, and the Kepler conjecture.
The IPA course is a hands-on course about using a proof
assistant to construct formal models of algorithms, protocols, and
programming languages and to reason about their properties. The
focus is on applying logical methods to concrete problems. The
course will demonstrate the challenges of formal rigour and the
benefits of machine support in modeling, proving and validating.
In the course, we will use the Isabelle proof assistant. The course
is structured in two parts: The first part introduces basic
and advanced modeling techniques (functional programs, inductive
definitions, modules), the associated proof techniques (term
rewriting, resolution, induction, proof automation), and
compilation of the models to certified executable code. In the
second part, the students work in groups on a project
assignment in which they apply these techniques: they build a
formal model and prove its desired properties. The project lies in
the area of programming languages, model checking, and information
security.
Knowledge of
- Logic and natural deduction
- Modeling techniques
- Proof techniques
Skills to
- Effectively use a proof assistant to write precise and concise models and specifications (i.e., apply the above modeling techniques).
- Use the proof assistant as a tool for checking and analyzing such models and for taming their complexity (i.e., apply the above proof techniques).
- Extract certified executable implementations from specifications.
Competences to
- Create unambiguous formal models and analyse them.
- Discuss what it means for a program/algorithm/system/model to be correct and rigorously demonstrate correctness.
The course progresses from teaching (lectures with exercises) to
project work and finally preparation for presentation/oral exam:
▪ Lecture phase: lectures and exercises, formation of project
groups (4 weeks)
▪ Project phase: project work (4 weeks)
▪ Presentation and exam preparation (1 week)
See Absalon for the course literature.
It is expected that students have a working knowledge of
programming and programming languages corresponding to the course
Advanced Programming (AP) or equivalent.
Semantics and Types (SaT) is recommended, but not required.
Academic qualifications equivalent to a BSc degree is
recommended.
Students receive feedback from the instructors during the exercise sessions and during project work.
Students give each other feedback within the project groups.
As
an exchange, guest and credit student - click here!
Continuing Education - click here!
PhD’s can register for MSc-course by following the same procedure as credit-students, see link above.
- ECTS
- 7,5 ECTS
- Type of assessment
-
Oral exam on basis of previous submission, 30 minutes (no preparation time)
- Type of assessment details
- Specifically, the exam consists of two parts:
1. Submission of the developed Isabelle formalization as part of the group project (written assignment).
2. An individual oral examination (without preparation) based on the project work (with a special emphasis on the part of the project the student has co-authored) and on the general course topics.
The project and oral examination are not weighted, and thus only a single overall assessment is provided for the two parts of the exam. - Aid
- All aids allowed
- Marking scale
- 7-point grading scale
- Censorship form
- No external censorship
Several internal examiners
- Re-exam
-
Same as the ordinary exam.
For the re-exam, the student must complete and submit a similar project to the regular one. The deadline for submitting the new report is 2 weeks before the re-exam.
Criteria for exam assessment
See Learning Outcome
Single subject courses (day)
- Category
- Hours
- Lectures
- 16
- Exercises
- 24
- Project work
- 145
- Exam Preparation
- 20
- Exam
- 1
- English
- 206
Kursusinformation
- Language
- English
- Course number
- NDAK23006U
- ECTS
- 7,5 ECTS
- Programme level
- Full Degree Master
- Duration
-
1 block
- Placement
- Block 1
- Schedulegroup
-
C
- Capacity
- No limitation – unless you register in the late-registration period (BSc and MSc) or as a credit or single subject student.
- Studyboard
- Study Board of Mathematics and Computer Science
Contracting department
- Department of Computer Science
Contracting faculty
- Faculty of Science
Course Coordinator
- Dmitriy Traytel (7-7775647c77686f43676c316e7831676e)
Teacher
Dmitriy Traytel
Are you BA- or KA-student?
Courseinformation of students