Length: 10 hours - 2 cfu
Abstract
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 "https://momigliano.di.unimi.it/IITP/iitp.html"
prerequisites: 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)
Dates & Venue
| Giorni | Aula | Orario |
| 21/02/2022 | Lab. Laurea Magistrale 3° floor - Via Celoria 18 - 20133 Milan | 10:00-12:00 |
| 23/02/2022 | Lab. Laurea Magistrale 3° floor - Via Celoria 18 - 20133 Milan | 10:00-12:00 |
| 25/02/2022 | Lab. Laurea Magistrale 3° floor - Via Celoria 18 - 20133 Milan | 10:00-12:00 |
| 28/02/2022 | .Lab. Laurea Magistrale 3° floor - Via Celoria 18 - 20133 Milan | 10:00-12:00 |
| 02/03/2022 | Lab. Laurea Magistrale 3° floor - Via Celoria 18 - 20133 Milan | 10:00-12:00 |