The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Coq Workshop

Second Call for informal presentations and demonstrations

The Coq workshop will take place on July 9th, as part as the FLoC 
federated conference in Edinburgh, Scotland.

<http://coq.inria.fr/coq-workshop/2010/cfp>


The Coq workshop will bring together Coq users, developers and 
contributors. The workshop will be organized from submitted, informal 
presentations, invited talks and a plenary discussion on the evolution 
and design of Coq.  Topics of presentations may include any of the 
following ones:

 * Experiments with type-theoretic proof assistants
 * Language or tactics features
 * Theory and implementation of the Calculus of Inductive Constructions
 * Applications and experience in education and industry
 * Tools, platforms built on Coq
 * Plugins, libraries for Coq
 * Interfacing with Coq
 * Formalization tricks and Coq pearls

Topics that have been experimented with in any flavor of type 
theory-based theorem proving and are relevant to the evolution of Coq 
may also be discussed during these informal presentations.

Speakers wishing to present a demonstration should bring their own 
laptop computer or contact the program chair to arrange for a computer 
to host the demonstration.

Descriptions of the proposed informal presentations should consist of 
abstracts of  approximately 1000 words and be uploaded to the easychair 
system

<http://www.easychair.org/conferences/?conf=coq2>

before May 10th.

For further questions, please contact Yves Bertot.

Yves.Bertot AT sophia.inria.fr