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 for research students about course offerings
VT2024 and then based on demand
About course offering
For course offering
Spring 2024 Start 18 Mar 2024 programme students
Target group
No information insertedPart of programme
No information insertedPeriods
P4 (7.5 hp)Duration
18 Mar 2024
3 Jun 2024
Pace of study
50%
Form of study
Distance Daytime
Language of instruction
English
Course location
KTH Campus
Number of places
Places are not limited
Planned modular schedule
Course memo
Course memo is not publishedSchedule
Schedule is not publishedApplication
For course offering
Spring 2024 Start 18 Mar 2024 programme students
Application code
61122
Contact
For course offering
Spring 2024 Start 18 Mar 2024 programme students
Examiner
No information insertedCourse coordinator
No information insertedTeachers
No information insertedHeadings 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.
Equipment
A computer
Literature
The primary literature will be the online book “Software Foundations”, which also contains theorem-proving exercises: https://softwarefoundations.cis.upenn.edu/.
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
Opportunity to complete the requirements via supplementary examination
No information inserted
Opportunity to raise an approved grade via renewed examination
No information inserted
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
Add-on studies
No information inserted