Second Coq Implementors Workshop, May 30 - June 3, 2016, Sophia-Antipolis

This page collects useful infos for the participants to the second Coq Implementors Workshop.

The Coq Implementors Workshop is an event that brings together the core developers of Coq and people willing to understand, improve or extend the system.


The Implementors Workshop takes place at the Inria Center in Sophia-Antipolis (how to reach the Inria center, accommodation infos).


Program PDF

Talks by devs:

Do log what you did/learnt/implemented!

Write it here.


For organization purposes we require the participants to register (free of charge) by subscribing to the coordination mailing list.

The mailing list is also the preferred channel to contact the organizers. Subscription is required in order to post.

Beach event


Quick list of dinner options

(pick what you prefer and build your dinner group around you)

List of participants

  1. Yves Bertot
  2. Maxime Dénès
  3. Enrico Tassi
  4. Pierre-Marie Pédrot
  5. Matej Košík
  6. Matthieu Sozeau
  7. Cyprien Mangin
  8. Guillaume Melquiond
  9. Pierre Letouzey
  10. Hugo Herbelin
  11. Emilio J. Gallego Arias
  12. Nicolas Magaud
  13. Pierre-Évariste Dagand
  14. Lionel Rieg
  15. Cyril Cohen
  16. Théo Zimmermann

(+) Late subscription (tradition says you pay a round at the pub...)

Bug squashing

A list of relatively simple bugs, to kill the time ;-)

Also, bug triaging is very welcome (check if a bug is still valid, add extra info, close solved bugs...).

"Little" projects

Finish the safe string patch

A good little project is to submit some cleanups for -safe-string as hinted in

Fix Ocaml Warnings

Compiling Coq with Ocaml Warning enabled provides interesting cases to look at for cleanups. More details in Bug:

A special interesting project is to get the kernel to compile warning clean with *all warnings enabled*.

Using Merlin is highly recommended for this task.

Remove redundant typing

In 8.4 setoid_rewrite, there was code to type-check terms known to be well-typed. It would be useful to scan the codebase to look for other redundant type-checks.

Brainstorming ("harder" projects, to be considered carefully)


Individual Projects

Insert here your individual plan for the week:

Emilio J. Gallego Arias

Discussion on the roadmap

The changes we should discuss during the implementors workshop are:

Cocorico: CoqImplementorsWorkshop/CoqIW2016 (last edited 10-03-2017 14:18:21 by ron)