Introduction to Interactive Theorem Proving with Coq
A.Y. 2021/2022
Course offered to students on the PhD programme in
Visit the PhD website for the course schedule and other information
Lead instructor: Alberto Davide Adolfo Momigliano
We give an overview of interactive theorem proving with the Coq proof assistant, applied to the verification of software correctness. We will also touch upon the integration of testing and proving. Our main examples are drawn from the theory of programming languages, by mechanizing the specification of programming languages and their semantics, and by reasoning over individual programs as well as over generic program transformations, as typically found in compilers. Details can be found at "https://momigliano.di.unimi.it/IITP/iitp.html"
Familiarity with functional programming (Ocaml, Haskell, but Python may suffice); basic knowledge of first-order logic; interest (if not competence) in the semantics of programming languages (interpreters, type systems, compilers)
Assessment methods
Giudizio di approvazione
Assessment result
superato/non superato
How to enrol
Deadlines
The course enrolment deadline is usually the 27th day of the month prior to the start date.
How to enrol
- Access enrolment on PhD courses online service using your University login details
- Select the desired programme and click on Registration (Iscrizione) and then on Register (Iscriviti)
Ignore the option "Exam session date” that appears during the enrolment procedure.
Contacts
For help please contact [email protected]
Professor(s)
Reception:
by appointment