CoqWG20160928
The Working Group took place on September 28th and 29th room A215 of Inria Paris (2, rue Simone Iff) on the 28th and at Sophie Germain, PPS on the 3rd floor on the 29th.
Videos of some of the talks are available here: https://www.youtube.com/watch?v=JCdUDB_2VwE
-
10:00 - 10:15 Packages, libraries, standard library (Hugo Herbelin)
Gathering opinions about the issues raised recently on these topics.
-
10:15 - 10:30 A "recommended" programming style (Hugo Herbelin)
Is there more to say on PR#267?
-
10:30 - 11:00 SerAPI overview (Emilio Jesús Gallego Arias)
-
11:00 - 11:15 Break
-
11:15 - 11:45 Error handling in the XML/STM protocol (Emilio Jesús Gallego Arias)
-
11:45 - 12:00 Unifying unifiers (Matthieu Sozeau)
Progress report
-
12:00 - 12:30 Remaining bugs in 8.6 (Maxime Dénès)
-
12:30 Lunch
-
Afternoon: bug squashing for 8.6
-
18:30 Social event at Brewberry
-
10:00 - 10:30 From small inversion to pattern-matching compilation (Hugo Herbelin, Meven Bertrand)
-
10:30 - 10:45 Rewriting strategies, coqrel and transfer (Matthieu Sozeau, Jérémie Koenig, Théo Zimmermann)
-
10:45 - 11:00 coq_makefile in Coq 8.7 (Enrico Tassi)
a meta-meta-language is a bit too much for my little brain
-
11:00 - 11:15 Break
-
11:15 - 11:30 Defining a few policies (Maxime Dénès)
- Moving to OCaml 4.03
- Renaming "trunk" to "master"
- How many compat flags?
-
11:30 - 12:00 Group therapy
discussion on difficult bugs that could not be solved the previous day, or revealed other problems (if any)
-
12:00 Lunch
-
Afternoon: more bug squashing for 8.6
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq 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.