Introduction The quest for correctness Computer aided formal reasoning Proof assistants The Coq proof assistant 1 The Coq proof assistant 2 The Coq proof assistant 3 Coq paraphernalia Other proof assistants: Coq's Siblings Other proof assistants: Coq's Cousins Coq languages: Gallina and the vernacular Some Gallina More Gallina Some vernacular: normal mode Some vernacular: switching to proof mode Some vernacular: back from proof mode More vernacular: inductive definitions A proof example: excluded middle implies Peirce's law LEM implies Peirce's law 1 LEM implies Peirce's law 2 LEM implies Peirce's law 3 LEM implies Peirce's law 4 LEM implies Peirce's law 5
