The Coq proof assistant is an interactive theorem prover based on the calculus of inductive constructions, a type theory with dependent types also allowing inductive definitions.
In this lecture, we start with some theoretical background introducing constructive logic and the Curry-Howard correspondence. Then we take a more practical approach and study how to write specifications, define data types, as well as how to compute and reason about these data types within Coq. Finaly, we present a demo showing how one actually proceeds to develop proofs interactively in Coq.
| Nicolas Magaud |
| Nicolas Magaud is a post-doctoral research associate with PLS team in the School of Computer Science and Engineering at UNSW and is currently working in the Sec project. |
| Date: | Mon Sep 6 2004 |
| Time: | 10:30am to 12:00pm |
| Location: | G3, Electrical Engineering (UNSW) RSISE Video Conference Room; A207, building 115, cnr. North and Daley Roads (ANU) |
Last updated by rhuuck at Fri Sep 3 13:29:49 2004 GMT+1000