From Camp 2011 Public Wiki
| Coq Workshop | |
|---|---|
| This will be more or less a hands-on version of the "Certified programming with dependent types" talk. I'll try to show how to use Coq for programming and work through some basic proving examples.
Workshop language will be German, unless English is requested. Actual starting time will be after the lightning talks, probably closer to midnight. | |
| Organizer | [[Has organizer::User:Nobody]] |
| Contact | xmpp:nobody@jabber.berlin.ccc.de |
| DateTime | Day 4 / Aug 13 @ 23:30 |
| Duration | 2:00 + |
| End | Error: invalid timewarning.pngThe date "<strong class="error">Error: invalid time</strong>" was not understood. |
| Location | Mojave |
Prerequisites
Pleas pre-install coq and either coqide or emacs and proofgeneral with coq support. Most Linux distros have these in their package repo.
I'm a vim user, I'll be using coqide. On Ubuntu, proofgeneral should Just Work (tried it), but if you're running into problems I probably won't be able to help.
Windows and Mac OS users go to [1].
Once you're set up, please create a file 'test.v' with the following contents and open it with coqide or proofgeneral.
Require Import Omega. Theorem foo : forall m n o, m > n -> n > o -> m > n. Proof. intros; omega. Qed.
If you can step through the code (emacs: C-c C-n) and get back some info from the system, everything's fine. Otherwise, please tell me right away so we can fix things. (I don't have DECT, but I should be online (Jabber) all the time until the workshop.)
If things don't work, consider bringing a Ubuntu live disk / USB stick, if it boots it should work and be fast enough for this.
Links
The Coq Website.
IMO, the following are the three most important resources for learning how to use coq:
- Software Foundations tutorial by B. Pierce and others: Starts pretty much from zero, offers many examples and exercises. Probably enough to get you started.
- Coq'Art - Interactive Theorem Proving and Program Development (book): More theoretical explanations, starts close to zero. IMO not suitable as a first tutorial, but great if you're working with Coq.
- Certified Programming with Dependent Types by Adam Chlipala: Mind-boggling explanations and examples, thorough explanations on how to automate proofs. Read this last.
If you're stuck, there's an IRC channel on freenode and there are a couple of knowledgeable users on stackoverflow.
