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 (https://www.portauxrocs.com/).
More details can also be found attachment:brochure.pdf.
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 (attachment:ligne_bus.pdf).
== Program == . The schedule will run from monday afternoon to friday after lunch.
Tentative https://docs.google.com/spreadsheets/d/1mUtbJHJUKvwyUsp0cNGpTpdErpaxNqjk4TEPjrvIdIg/edit?usp=sharing
Talks by devs:
- Unification (Matthieu)
- Cumulative inductive types (Amin, Matthieu)
##attachment:schedule.pdf ##Talks by devs:
* Introduction (Enrico, Maxime, Matej) attachment:intro.pdf
* STM (Enrico) attachment:stm4hackers.pdf
* Extraction (Pierre L) attachment:extraction.pdf attachment:extraction_demo.v attachment:extraction_cornercases.v attachment:explicit_cumul.v
* Notations (Hugo) attachment:notations.pdf
* Universes (Matthieu) attachment:universes.pdf (see dev/doc/univpoly.txt too)
* Ltac (Pierre-Marie) attachment:ltac-internals.pdf
== Do log what you did/learnt/implemented! == Write it https://coq.inria.fr/cocorico/CoqImplementorsWorkshop/CoqIW2017/log.
== Registration == To register, please fill in the following http://gipco-adns.com/site/5922/coqdev+2017+registration+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 https://sympa.inria.fr/sympa/info/coq-implementors-workshop 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...)
== Proposed Projects and Ideas ==
- By EJGA:
- New internal document format for the STM.
- Plugin linking with external deps.
- Language Server Protocol support.
- Ocamlbuild for Coq + bisect_ppx support.
- SerAPI OPAM.
- Glob_constr vs constrexpr rework (upcoming CEP).
- Data-centric CRUD API.
- Auto deploy from Travis.
- Travis Build Stages
- Windows CI (appveyor)
- Support for notation tables
- ENotation (Extended Notation Display)
- By MS:
- Specification/documentation of unification
- By TZ:
- Combining focusing with { } and goal selectors (started https://github.com/Zimmi48/coq/tree/testing_brackets_with_goal_selector).
- 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 topic by Paul:
- Resolving variable shadowing conflicts, Bug 5448
- By Abhishek Anand: (the items are below are needed in the implementation of https://arxiv.org/abs/1705.01163)
- https://sympa.inria.fr/sympa/arc/coq-club/2017-02/msg00059.html
- https://github.com/gmalecha/template-coq/issues/1
- By Yves
- port coq-dpdgraph to more recent version of Coq (trunk and pre-8.7) https://github.com/Karmaki/coq-dpdgraph == 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)
- ...
To the extent possible under law, the contributors of the Rocq wiki have waived all copyright and related or neighboring rights to their contributions.
By contributing to the Rocq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.