What is this course about?
- The precise art of formal reasoning.
- Use a proof assistant (COQ) to formalize proofs.
- Propositional logic as the scaffolding of reasoning
- Foundational issues: classical vs intuitionistic logic
- Express yourself precisely
using the language of predicate logic
- Finite sets and operations on sets, reasoning by cases.
- Reasoning about natural numbers, proof by induction
- Equational reasoning (Algebra).
- Reasoning about programs and data structures.
What is Coq ?
- COQ: a Proof Assistant based on the Calculus of Inductive Constructions}
- Developed in France since 1989.
- Growing user community.
- Big proof developments:
- Correctness of a C-compiler
- 4 colour theorem
Why using a proof assistant?
- Avoid holes in paper proofs.
- Aid understanding. What is a proof?
- Formal certification of software and hardware.
- Download COQ from http://coq.inria.fr/
- Runs under MacOS, Windows, Linux
- coqtop : command line interface
- coqide : graphical user interface
- proof general : emacs interface
- coqtop and coqide installed on the lab machines
- Coq Reference manual: http://coq.inria.fr/V8.1pl3/refman/
- Coq Library doc: http://coq.inria.fr/library-eng.html
- Coq'Art, the book by Yves Bertot and Pierre Casteran (2004).
(available in the library!)
- Course page: http://www.cs.nott.ac.uk/~txa/g52ifr/
- Coq Labs: every Tuesday (1600 - 1800) in A32, starting next week (11/10).
- Weekly coursework, 1st available next Monday.
- Use online submission system (cw).
- Tutorials: start next week. See assignment on webpage.
- Online class test on coq in December.
- Online Forum: Information about coursework, discuss questions