CoqIW2017

Third Coq Implementors Workshop, June 12 - June 16, 2017, Le Croisic

This page collects useful infos for the participants to the third 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.

Location

The Implementors Workshop takes place at Port aux Rocs in Le Croisic.

More details can also be found here.

Going from Nantes to Le Croisic takes 1h20 by train. There are also direct train from Paris (3h20).

To go from Le Croisic railway station to Port aux Rocs, you can take Bus 30 schedule.

Program

The schedule will run from monday afternoon to friday after lunch.

Tentative schedule

Talks by devs:

• Introduction slides
• Cumulative inductive types (Amin Timany, Matthieu Sozeau)
• Definitional Proof-Irrelevance (Gaëtan Gilbert)
• Ltac 2 (Pierre-Marie Pédrot)
• Coq and User Interfaces (Emilio Jesus Gallego Arias) slides
• Parametricity in Coq (Abhishek Anand) slides
• ELPI (Enrico Tassi)
• The beautifier and notations (Hugo Herbelin) slides

PRs to discusss:

• Binding of universe constraints https://github.com/coq/coq/pull/688
• eauto https://github.com/coq/coq/pull/721
• Warning on names generated by Coq https://github.com/coq/coq/pull/268
• ...

Do log what you did/learnt/implemented!

Write it here.

Registration

To register, please fill in the following form.

The registration is 561€ (single bed room) or 443€ (twin bed room).

Registration comprises (per person):

• workshop attendance
• accommodation from Monday, June 12 to Friday, June 16 included (4 nights)
• all meals from Monday, June 12 to Friday, June 16 (lunch)
• coffee breaks
• gala dinner.

Registration deadline: May 10.

The registered participants will receive a notification of their registration by e-mail. Participants who are unable to attend the workshop should send an e-mail to the organizers as soon as possible and contact the hotel directly.

Methods of payment

By credit card, on site.

By cheque addressed to: Domaine de Port-aux-Rocs and sent to: Domaine de Port-aux-Rocs A l'attention de Madame Laetitia Gillet 44 avenue de Port Val 44490 Le Croisic

By "bon de commande" (organismes publics français uniquement) addressed to the address above. If you need a quote or more information about your payment, please send an e-mail to Port-aux-Rocs

IMPORTANT: For payments by cheque or bon de commande, please indicate the reference « 53163-35753 » on your payment.

If you need funding to attend the workshop, please contact the organizers to see what is possible.

Organizers

• Maxime Dénes (mail at maximedenes.fr)
• Matthieu Sozeau (matthieu.sozeau at inria.fr)
• Nicolas Tabareau (nicolas.tabareau at inria.fr)

The coordination mailing list is the preferred channel to contact the organizers.

If you need additional funding, please contact the organizers.

List of participants

• Abhishek Anand
• Yves Bertot
• Simon Boulier
• Maxime Dénès
• Yannick Forster
• Emilio Jesús Gallego Arias
• Gaëtan Gilbert
• Hugo Herbelin
• Ambroise Lafont
• Cyprien Mangin
• Thierry Martinez
• Pierre-Marie Pédrot
• Matthieu Sozeau
• Kathrin Stark
• Nicolas Tabareau
• Enrico Tassi
• Amin Timany
• Théo Winterhalter
• Théo Zimmermann

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

Suggestions by New Participants

I [EJGA] performed an informal poll asking new participants what they thought of the IW and how we could improve for next year. The conclusion was that it would be good to have ready a concrete set of projects for people new to Coq and to hold a small session where each new participant gets to pick a project and a mentor. They told me they had the hardest time figuring out what to do. Other than that their experience was very positive.

Proposed Projects and Ideas

• By EJGA:
  • New internal document format for the STM, functional-state handling. [my main focus for this IW] (CEP012)
  • Glob_constr vs constrexpr rework (upcoming CEP011).
  • Plugin linking with external dependencies.
  • Language Server Protocol support. Jupiter / IPython support.
  • Ocamlbuild for Coq
  • Code coverage with bisect_ppx.
  • SerAPI OPAM.
  • Data-centric CRUD API.
  • Auto deploy from Travis.
  • Travis Build Stages
  • Windows CI (appveyor)
  • Support for notation tables (notation scopes that can modify the parser)
  • ENotation (Extended Notation Display)
  • Scoping mechanism that is friendly to parallel processing.
  • Better benchmarking / timing for the batch compiler.
• By MS:
  • Specification/documentation of unification
  • A big TODO list!
• By TZ:
  • Combining focusing with { } and goal selectors (started here).
  • A way to easily give names to goals.
  • A strict mode that's satisfying for SSReflect (and for vanilla Coq as well if possible).
• By Enrico:
  • coq-elpi (Elpi embedded in Coq) and the GPWD
• Suggested discussion topics by Paul:
  • Resolving variable shadowing conflicts, Bug 5448
  • Unit testing to supplement end-to-end tests, including time, space usage
• By Abhishek Anand: (the items are below are needed in the implementation of paramcoq-iff)
  • Efficiency reducing away mentions of a variable
  • Supporting universes in Template-coq
• By Yves

  • port coq-dpdgraph to more recent version of Coq (trunk and pre-8.7)

    coq-dpdgraph github site

Topics of interest

• Simon Boulier : different ways of being opaque ; managing of universes ; Template Coq & plugins
• Overview Coq Source Code, Plugins
• more keywords vs fewer keywords (GPR #616)
• ...