The Coq Workshop 2013
The 5th Coq Workshop
A satellite workshop of ITP 2013, Rennes, July 22nd
The Coq Workshop series brings together Coq users, developers, and contributors. While conferences like ITP provide a venue for traditional research papers, the Coq Workshop focuses on strengthening the Coq community and providing a forum for discussing practical issues, including the future of the Coq software and its associated ecosystem of libraries and tools. Thus, the workshop will be organized around informal presentations and discussions, supplemented with invited talks. The program features two invited talks by Guillaume Melquiond and Bas Spitters. Bas Spitters' participation is funded by the European Commission FP7, STREP project ForMath, n. 243847.
|18:30 - 20:00||Welcome drinks reception at Le café des Camps libres, 10 Cours des Alliés, 35000 Rennes.|
The local organizers provide a map showing the way from the railway station (A) to Le café des Champs libres (B)
The workshop will take place at INRIA Rennes-Bretagne-Atlantique, on the university campus (called "Campus de Beaulieu"), in the east of Rennes. See here the practical informations provided by the local organizers.
|09:00 - 10:00||Guillaume Melquiond||Automations for verifying floating-point algorithms|
|10:00 - 10:30||Coffee|
|10:30 - 11:00||Catherine Lelay||A New Formalization of Power Series in Coq|
|11:00 - 11:30||Reynald Affeldt and Kazuhiko Sakaguchi||First Building Blocks For Implementations of Security Protocols Verified in Coq|
|11:30 - 12:00||Michael Nahas||A Decentralized Proof-term Library for Coq|
|12:00 - 13:45||Lunch|
|13:45 - 14:45||Bas Spitters||Formalizing mathematics in homotopy type theory|
|14:45 - 15:00||Break|
|15:00 - 15:30||Yves Bertot||Private Inductive Types|
|15:30 - 16:00||Jorge Luis Sacchini and Bruno Barras||Type-Based Methods for Termination and Productivity in Coq|
|16:00 - 16:30||Coffee|
|16:30 - 17:00||Maxime Dénès||Towards primitive data types for Coq: 63-bits integers and persistent arrays|
|17:00 - 17:30||Coq development team||invited talk|
Abstracts and slides
Sent on the coq-club, types-announce, caml-list and ssreflect mailing lists on Feb 07, Mar 29 and Apr 5 (last call). Text follows.
Subject: Call for proposals: The 5th Coq Workshop ================================================================================ The Fifth Coq Workshop (2013) http://coq.inria.fr/coq-workshop/2013 Colocated with the 4rd International Conference on Interactive Theorem Proving (ITP 2013), Rennes, France ================================================================================ The Coq Workshop series brings together Coq users, developers, and contributors. While conferences like ITP provide a venue for traditional research papers, the Coq Workshop focuses on strengthening the Coq community and providing a forum for discussing practical issues, including the future of the Coq software and its associated ecosystem of libraries and tools. Thus, the workshop will be organized around informal presentations and discussions, likely supplemented with invited talks. We invite all members of the Coq community to propose informal talks, discussion sessions, or any potential uses of the day allocated to the workshop. Relevant subject matter includes but is not limited to: * Language or tactic features * Theory and implementation of the Calculus of Inductive Constructions * Applications and experience in education and industry * Tools and platforms built on Coq * Plugins and libraries for Coq * Interfacing with Coq * Formalization tricks and Coq pearls Authors should submit short proposals through EasyChair. Submissions should be in portable document format (PDF). Proposals should not exceed 2 pages in length in single-column full-page style. Venue: ITP, Rennes. Important Dates: * April 7: Deadline for proposal submission * April 28: Acceptance notification * July 22: Workshop in Rennes Submission URL: https://www.easychair.org/conferences/?conf=coq5 Program committee: * Pierre Letouzey, Université Paris 7, France * Marco Maggesi, Università degli Studi di Firenze, Italy * Assia Mahboubi (co-chair), INRIA, France * David Pichardie, INRIA, France * Benjamin Pierce, University of Pennsylvania, USA * Randy Pollack, University of Edinburgh, UK * Enrico Tassi (co-chair), INRIA, France * Viktor Vafeiadis, MPI-SWS, Germany Contact: Assia Mahboubi (firstname.lastname@example.org), Enrico Tassi (email@example.com)