The course is centered around interactive lecture seminars and invited seminars (approximately 5 lecture seminars and 1-2 invited seminars). During the lecture seminars, both theoretical and practical aspects of interactive theorem proving will be discussed, focusing on the Coq proof assistant. In the invited seminars, external speakers present different aspects of other proof assistants. The primary learning activities are take-home exercises, where the student will conduct a substantial amount of theorem proving. At the end of the course, each student will give an oral presentation, reflecting on their experience of theorem proving, focusing on certain proofs performed during take-home exercises.
FID3217 Interactive Theorem Proving with Dependent Types 7.5 credits
In this course, you will learn the fundamentals of interactive theorem proving. Specifically, we will focus on the proof assistant Coq, learning both proof strategies for logical foundation and programming language semantics. The course is both theoretical and practical. Theoretically, the proof assistant is based on a sound theory of the calculus of inductive constructions. Fundamental aspects such as Curry-Howard correspondence and dependent types will also be discussed. The course is also practical: all students will work individually on a large set of theorem-proving exercises, thus learning the practical aspect of proof engineering. At the end of the course, the student will be able to conduct individual proof engineering using the Coq proof assistant in general and specifically within programming language theory.
Information per course offering
Course offerings are missing for current or upcoming semesters.
Course syllabus as PDF
Please note: all information from the Course syllabus is available on this page in an accessible format.
Course syllabus FID3217 (Spring 2024–)Headings with content from the Course syllabus FID3217 (Spring 2024–) are denoted with an asterisk ( )
Content and learning outcomes
Course disposition
Course contents
The course covers several aspects of interactive theorem proving, with a focus on the Coq proof assistant. Topics covered in the course include: induction, dependent types, Curry-Howard correspondence, tactics, polymorphism, inductive types, Hoere logic, small-step operational semantics, type systems, type checking, and the simply typed lambda calculus (STLC). Guest seminars may also discuss one or two other proof assistants, such as Isabelle/Isar, Lean, HOL, and Agda.
Intended learning outcomes
After the course, the student will be able to:
- Construct proofs in Coq related to basic logic
- Apply proof assistant tactics
- Construct proofs in Coq related to programming language semantics
- Explain the concept of dependent types
- Explain the differences between different kinds of proof assistants
- Explain and reflect on ethical aspects of mathematics in computer science
Literature and preparations
Specific prerequisites
None
Recommended prerequisites
A course in logic and a course in programming language semantics.
Literature
You can find information about course literature either in the course memo for the course offering or in the course room in Canvas.
Examination and completion
If the course is discontinued, students may request to be examined during the following two academic years.
Grading scale
P, F
Examination
- INL1 - Homework/Hand-in exercise/Hand-in assignment, 7.5 credits, grading scale: P, F
Based on recommendation from KTH’s coordinator for disabilities, the examiner will decide how to adapt an examination for students with documented disability.
The examiner may apply another examination format when re-examining individual students.
The examination is conducted using take-home exercises and a final presentation.
Other requirements for final grade
None
Examiner
Ethical approach
- All members of a group are responsible for the group's work.
- In any assessment, every student shall honestly disclose any help received and sources used.
- In an oral assessment, every student shall be able to present and answer questions about the entire assignment and solution.
Further information
Course room in Canvas
Registered students find further information about the implementation of the course in the course room in Canvas. A link to the course room can be found under the tab Studies in the Personal menu at the start of the course.
Offered by
Main field of study
This course does not belong to any Main field of study.
Education cycle
Third cycle