The Coq mailing list

[David MENTRÉ <dmentre AT linux-france.org>]

Hello,

I am doing some introductory course on formal methods. Amongst them, I 
tell a few words about Coq and its underlying principles.

To illustrate more concretely this Coq part, would somebody have or 
point me to some *very* simple Coq examples of:

 * Constructive logic: an example showing a short demonstration that 
exhibits the mathematical element to prove compared to the same proof 
made with classical logic;

 * Curry-Howard isomorphism: a very simple Coq theorem (on Boolean or 
integers) with associated proof, from which I could also generate OCaml 
code and show the Coq type.

The shorter the better. If both parts can be combined into the same 
example, it might be easier to explain.

I have looked on Wikipedia and Google but examples I found were rather 
complicated (at least not something that can be explained in one slide).

Many thanks in advance for any help.

Best regards,
david