The 1st Coq Workshop Munich, Germany 21 August, 2009 (a satellite workshop of TPHOLs 2009)

The Coq workshop will bring together Coq users, developers and contributors. It is organized from contributed papers, an invited talk and a plenary discussion on the evolution and design of Coq (see the call for papers). Journal versions of the workshop papers will be considered for publication as a special issue of the Journal of Formalized Reasoning.

Program

09:00-10:00 Invited talk (joint with PLMMS)

Ssreflect: Structured Scripting for Higher-Order Theorem Proving Georges Gonthier (abstract)

10:00-10:40 Coffee break
10:40-12:10 Contributed talks 1

A New Look at Generalized Rewriting in Type Theory Matthieu Sozeau
Descente Infinie Proofs in Coq Răzvan Voicu, Mengran Li
Sets in Coq, Coq in Sets Bruno Barras

12:10-13:40 Lunch
13:40-15:10 Contributed talks 2

A Tactic for Deciding Kleene Algebras Thomas Braibant, Damien Pous
Formalizing a SAT Proof Checker in Coq Ashish Darbari, Bernd Fischer, Joao Marques-Silva
Proof Objects for Logical Translations Andrew Polonsky, Marc Bezem

15:10-15:40 Coffee Break
15:40-16:00 Report on the development of Coq (document)
16:00-17:10 Discussion (summary)

The workshop is supported by the Coq Technological Development Action (at INRIA) which thanks the Technical University of Munich for its local support and for pre-publishing the proceedings.