Contenu de la matière
I. Introduction to lambda-calculus II. Simple and Higher order types theory III. Constructive logic IV. Introduction to Coq assistant theorem prover V. Introduction to QWIRE programming VI. Implementing QWIRE in Coq