[TYPES/announce] Coq-Workshop: Call for informal presentations (updated information)

[Yves Bertot]

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