Coq Users and Developers Workshop 2019

Fifth Coq Users and Developers Workshop, June 3rd - June 7th, 2019, Sophia-Antipolis (Nice, France)

This page collects useful infos for the participants to the 5th Coq Users and Developers Workshop.

The Coq Users and Developers Workshop is an event that brings together the core developers of Coq and people interested in understanding, improving or extending the system.

Location

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

Sponsors

This workshop is sponsored by Inria.

Program (TBA)

The schedule will run from Monday afternoon (1pm) to Friday after lunch (~ 2pm). We will have lunch at the Inria cafeteria.

Gitter room

https://gitter.im/coq/CUDW2019

This is the preferred channel for public discussion with other participants and with the organizers. Feel also free to contact the organizers directly by e-mail.

Registration

Registration to this event is free but mandatory for organization purposes. To register you should simply add your name in the list of participants below.

Please include your e-mail address (in a human readable form).

• Frédéric Dabrowski (frederic.dabrowski at univ-orleans.fr)
• Maxime Dénès (maxime.denes at inria.fr)
• Michael Soegtrop (michael dot soegtrop at intel.com)
• Théo Zimmermann (theo at irif.fr)
• Claude Stolze (claude.stolze at inria.fr)
• Gaëtan Gilbert ([email protected])
• Kazuhiko Sakaguchi ([email protected])
• Jim Fehrle (jim.fehrle at gmail.com)
• Frédéric Besson ([email protected])
• Enrico Tassi ([email protected])
• Ahmed Alharbi ([email protected])
• Pierre-Marie Pédrot ([email protected])
• Sorin Stratulat ([email protected])
• Lasse Blaauwbroek (lasse at blaauwbroek dot eu)
• Simon Boulier ([email protected])
• Talia Ringer ([email protected]) (staying at "Le Pré Catalan" in Antibes/Juan-les-Pins)
• Matthieu Sozeau (matthieu.sozeau at inria.fr) (staying at "Le Pré Catalan" in Antibes/Juan-les-Pins)
• Yannick Forster ([email protected])
• Cyril Cohen (cyril.cohen at inria.fr)
• Hugo Herbelin (Hugo.Herbelin at inria.fr)
• Karl Palmskog (palmskog at utexas.edu)
• Yves Bertot (Yves.Bertot at inria.fr)

Organizers

• Maxime Dénès (maxime.denes at inria.fr)

If you need additional funding, please contact the organizers.

Proposed Projects and Ideas

• @ejgallego: I'd like to a recreation of my current dev setup from scratch, and record it so it can be watched in Youtube. This setup includes a fully composed build, mu-repo, and some other goodies.

• @ejgallego: I'd like to see a demo of Octobox and other ideas / tools people use in managing their Github/Gitlab workflows. @Zimmi48: I'd be happy to do such a demo.

• @jfehrle: I'd like to investigate/discuss: 1) what it would take to get Coq to accurately report the series of tactics applied by auto or Ltac and 2) given a proof term, how difficult it would be to produce a list of tactics that generates the proof term. I think these could be useful both to beginners and experienced users and would make Coq tactics somewhat less of a black box.

• @fajb: I'd like to discuss what could be done to help debugging a failure of the CI. Currently, I find it very painful and time consuming. In my dreams, the CI would generate a minimal repro case which I could run on my local machine. Another dream would be to get the exact instant where the failing proof and a succeeding proof diverge.

• @sorinica: I would like to know the technical details that allow to integrate cyclic induction reasoning in Coq.

• @ppedrot: I am willing to work on https://github.com/coq/ceps/pull/40

• @mattam82: I'd like to reorganize the reference manual.

• @tlringer: I have a lot of Coq plugins that are not on the latest Coq version and are not in the CI. I would love to spend a day or two actually doing the work to get them all into the CI.

• @tlringer: I am also interested in proof optimization. I have some work in progress on this, and would love to complete it and run it on the standard library to find more efficient proofs. I would also love to talk to anyone who is interested in proof optimization.

• @tlringer: I am also interested in developing versions of rewrite and simpl that are more powerful and offer more control. I have a lot of rewriting and refolding machinery in my plugins that can help with this.

• @tlringer: I have a lot of completed work on automatically searching for and proving certain kinds of equivalences between types. If any of this is interesting, I am willing to contribute it back to Coq instead of keeping it in a plugin only, and I think that would be fun. I would also enjoy extending it to discover and prove new equivalences and relations between types that I do not currently support.

• @gares: problems with OPAM, user experience with nix (with @CyrilCohen). Wondering about having the opam-coq-archive automatically translated to nix, published and have instructions on using nix.

• @Zimmi48: will be happy to talk to people and give a hand on various projects (@fabj on CI, @mattam82 on the manual, @gares on Nix, @palmskog on automation for coq-community).