The Coq mailing list

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

Coq Workshop

Call for informal presentations and demonstrations

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 be uploaded 
to the easychair system

<http://www.easychair.org/conferences/?conf=coq-2>

before May 10th.

For further questions, please contact Yves Bertot.

Yves.Bertot AT sophia.inria.fr