Course at Summer School on Cryptography, Blockchain, and Program Verification, Mathinfoly 2019 at INSA, Lyon on 27-31 August 2019
Teaching team: Cătălin Hriţcu, Roberto Blanco, Florian Groult, Jérémy Thibault, Exequiel Rivas, and various local helpers.
This course will give a gentle introduction to: 1. logic and proofs, 2. functional programming, and 3. program verification. The most interesting aspect of this course is the use of the Coq proof assistant to write functional programs and to prove logical theorems about these programs, in a way that is one hundred percent formalized and machine-checked. The course will follow the 1st half of the Logical Foundations book (i.e., Volume 1 of the Software Foundations series). The students will learn the most by solving Coq exercises, from very simple to more interesting ones. The course will also give an overview of the practical successes of functional programming (e.g., the Tezos blockchain implementation is written in OCaml) and of verification in proof assistants like Coq (from machine-checked proofs of mathematical results such as the 4-color theorem to the CompCert verified compiler). We will end with an introduction to the Curry-Howard correspondence, a deep and beautiful connection between functional programs and logical proofs, which lies at the heart of the Coq proof assistant.
We will follow a slightly modified version of the Logical Foundations book, which is available here.
Tuesday, 27 August 2019:
Wednesday, 28 August 2019:
Thursday, 29 August 2019:
Friday, 30 August 2019: