[ The Types Forum (announcements only),
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.
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
* 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
before May 10th.
For further questions, please contact Yves Bertot.