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.
Program
Sunday 21
| Time | Activity |
|---|---|
| 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)
Monday 22
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.
| Time | Author | Title |
|---|---|---|
| 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
Guillaume Melquiond: Automations for verifying floating-point algorithms
Abstract:
Floating-point numbers are limited both in range and in precision, yet
they are widely used as a way to implement computations on real numbers.
Thus arithmetic operations cause small errors that might be amplified
during subsequent computations. As such, it is important to guarantee
that the computed values are still close enough to the ideal results.
The traditional way to tackle the verification of such programs is to
perform an error analysis, possibly using automated tools.
Unfortunately, when it comes to the low-level floating-point functions
found in mathematical libraries, the code is usually so contrived that
this approach falls short. Falling back to a pen-and-paper proof makes
it possible to verify such functions, but this process is long, tedious,
and error-prone. Formal proofs take care of that last point, but they
come at an even greater cost for the user. Thus one needs to recover
some automations inside proof assistants to ease the verification
process.
This talk will present an overview of some of the methods available for
the Coq proof assistant. In particular, it will focus on Gappa and some
other interval-based automations. The presentation will not really be
about the inner workings of these methods, but rather show how they can
be used in practice to verify some floating-point algorithms in Coq.
Slides:
Reynald Affeldt and Kazuhiko Sakaguchi: First Building Blocks For Implementations of Security Protocols Verified in Coq
Abstract: Pdf
Slides: Download
Bas Spitters: Formalizing mathematics in homotopy type theory
Abstract:
I will discuss some of the exciting developments in homotopy type theory
as presented in the book on the topic, as well as give a short overview of
some parts of the Coq library.
Slides: Download
Jorge Luis Sacchini and Bruno Barras: Type-Based Methods for Termination and Productivity in Coq
Abstract: Pdf
Slides: Download
Maxime Dénès: Towards primitive data types for Coq: 63-bits integers and persistent arrays
Abstract: Pdf
Slides: Download
Coq development team: invited talk
Abstract:
Slides: Download
Call
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 (assia.mahboubi@inria.fr), Enrico Tassi (enrico.tassi@inria.fr)
Syndicate