An initiation to Coq
by Paul Brauner (LORIA, INRIA, LaBRI, ENSEIRB-MATMECA)

• Paul Brauner Coq Introduction;
• older presentation in French
• Paul Brauner Coq demo:
• demo.v,
• sort.v;
• Paul Brauner Coq directory.

Older References

• Coq proof assistant (Coq at ENSEIRB, pointers to INRIA documentation, tutorials, exercises, slides (Gérard Huet));
• Coq session 1 (2006-2007) by pyg.