Du är inte inloggad på KTH så innehållet är inte anpassat efter dina val.
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.
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.
After the course, the student will be able to
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.
The examination is conducted using take-home exercises and a final presentation.
Whether you are taking the course for credits or not, please register by submitting the following form. Please check out the course info slides below for details on which exercises need to be done as part of the course.
All course assignments are available as part of the online book Software Foundations. Please check out the course info slides below for details on which exercises need to be done as part of the course. Note: you are only allowed to select, solve, and hand in exercises that result in Coq solutions, not theoretical exercises with written or pen-and-paper solutions.
You should download and solve the Coq exercises in-place within the Coq files. That is, download the .tgz files and change in-place within the files where it says, e.g., (* FILL IN HERE *). If you solve an exercise, you must mark it as solved, by adding the string [SOLVED] for the exercise, exactly like this:
(** **** Exercise[SOLVED]: 3 stars, standard (optimize_0plus_b_sound)
There are two rounds for submitting the exercises and one deadline for the reflection report (all deadlines are end-of-day, Swedish time).
For each volume, please submit the exercises as a Zip-file including ALL files within the original bundle, where you have modified the Coq-files according to the above. You submit the exercises by simply attaching the Zip-file and sending an email to dbro@kth.se. Likewise, you submit the reflection report as a PDF file. For details of the content of the submission, see the first lecture slide. If you, for some reason, cannot meet the deadline, please send an email to me before the deadline has passed so that we can find an individual plan.
You can find all the lectures' videos on this YouTube playlist.
All lecture seminars will be given over Zoom using room: https://kth-se.zoom.us/j/68443433212
Lecture Seminar 1: Course Information and Introduction to Coq
Examiner: David Broman
Teacher: Elias Castegren
Date: Monday, April 15, 17.00-19.30 (Stockholm), 8.00 am-10.30 am (California)
[Slides - Course info] [Video - Course info]
[Slides - Coq introduction] [Video - Coq introduction]
[Lecture Exercise]
Lecture Seminar 2: Coq and the Curry-Howard Correspondence
Teacher: Elias Castegren
Date: Thursday, May 2, 17.00-19.00 (Stockholm), 8.00 am-10.00 am (California)
[Slides] [Video]
Guest Lecture: Introduction to Agda
Teacher: Jeremy Siek, Indiana University, USA
Date: Tuesday, May 14, 17.00-19.00 (Stockholm), 8.00 am-10.00 am (California)
[Slides] [Video] [Code]
Lecture Seminar 3: Coq, Tactics, and Locally Nameless Representations
Teacher: Elias Castegren
Date: Thursday, May 23, 17.00-19.00 (Stockholm), 8.00 am-10.00 am (California)
[Slides] [Video] [Code]
Guest Lecture: Introduction to HOL
Teacher: Magnus Myreen, Chalmers, Sweden
Date: Thursday, June 4, 17.00-19.00 (Stockholm), 8.00 am-10.00 am (California)
[Slides][Video][Code]
Lecture Seminar 4: Programming Language Foundation part 2 in Coq
Teacher: Elias Castegren (Coq lecture)
Date: Thursday, June 13, 17.00-19.00 (Stockholm), 8.00 am-10.00 am (California)
[Slides][Video][Code]
Lecture Seminar 5: Final Student Presentations and Ethics
Teachers: David Broman and Elias Castegren
Tentative Date: Tuesday, June 25, 16.00-19.00 (Stockholm)