Course ObjectiveThis course will provide an introduction to the practice of formalizing
mathematics in dependent type theory, using an interactive proof
assistant and its library. The course will be based on the proof
assistant Coq and its Mathematical Components library.
Course ContentProof assistants are pieces of software for doing machine-assisted
mathematics and for developing digital libraries of formalized
mathematics. This course will provide an introduction to the foundations
and practice of the Coq proof assistant. It will include a primer to
dependent type-theory, the logical formalism underlying a family of
popular proof assistants like Lean, Agda, Matita, and Coq. The course
will start with a gentle introduction to the art of writing formal
statements and proofs. Then, it will present the concepts and
formalization techniques at stake in the representation of mathematics
in dependent type theory. Hands-on sessions will address concrete
formalization examples, both in computational mathematics and in purely
Teaching MethodsIntensive course interleaved with hands-on sessions 5h a day for 3 days.
Personal laptop mandatory (but no software installation required).
Lectures will take place 17-19-21 Feb.
Method of AssessmentTwo small hand-in examinations, to be handed on 19 and 21 Feb.
respectively, count for 30% of the final grade. A final on-site hands-on
test, on Feb. 28th, counts for 70% of the final grade.
Target AudienceMSc students in Mathematics. Interested MSc students from other
disciplines, especially (Theoretical) Computer Science, are also
welcome. As are advanced motivated BSc students.
Recommended background knowledgeNo previous experience with formal verification and no background in
functional programming is required. Ability to understand and write down
detailed mathematical proofs in general, is expected.
|Language of Tuition||English|
|Faculty||Faculty of Science|
|Course Coordinator||dr. A.S. Mahboubi|
|Examiner||dr. A.S. Mahboubi|
dr. A.S. Mahboubi
You need to register for this course yourself
Last-minute registration is available for this course.
|Teaching Methods||Seminar, Computer lab, Lecture|
This course is also available as: