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:00Welcome 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:
Catherine Lelay: A New Formalization of Power Series in Coq Abstract: Pdf Slides: Download
Reynald Affeldt and Kazuhiko Sakaguchi: First Building Blocks For Implementations of Security Protocols Verified in Coq Abstract: Pdf Slides: Download
Michael Nahas: A Decentralized Proof-term Library for 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
Yves Bertot: Private Inductive Types Abstract: Pdf 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)