Material for the Cirm school on the Semantic of Proofs and Certified Mathematics:
- First course: types, terms in CIC, basic inductive types
- Second course: introduction to the formalization of HoTT
- no slide, we provide a formalized account of the proofs from Thierry's two first lectures
- ssreflect or plain Coq scripts of the lecture
- exercises
- ssreflect tactics cheat sheet for tactics.
- Third course: reflection