CoqWG20170306
The Working Group is taking place on March 6th and 7th at Inria Paris (2, rue Simone Iff). The room is "Jacques-Louis Lions 2".
Monday morning: Yves Bertot, Maxime Dénès, Daniel de Rauglaudre, Emilio Jésus Gallego Arias, Hugo Herbelin, Matej Košík, Pierre Letouzey, Cyprien Mangin, Guillaume Melquiond, Pierre-Marie Pédrot, Matthieu Sozeau, Enrico Tassi, Amin Timany, Théo Zimmermann.
Monday afternoon: Yves Bertot, Roberto Blanco, Maxime Dénès, Emilio Jésus Gallego Arias, Georges Gonthier, Hugo Herbelin, Matej Košík, Pierre Letouzey, Assia Mahboubi, Cyprien Mangin, Guillaume Melquiond, Pierre-Marie Pédrot, Thomas Pinot-Sibute, Sylvain Ribstein, Matthieu Sozeau, Enrico Tassi, Amin Timany, Théo Zimmermann.
Tuesday morning: Yves Bertot, Maxime Dénès, Emilio Jésus Gallego Arias, Georges Gonthier, Matej Košík, Pierre Letouzey, Assia Mahboubi, Cyprien Mangin, Guillaume Melquiond, Pierre-Marie Pédrot, Thomas Pinot-Sibute, Matthieu Sozeau, Enrico Tassi, Amin Timany, Théo Zimmermann.
- 9:00 Coffee
- 10:00 Contributors, past and present (Matthieu Sozeau)
- 10:30 A quick report on 8.7 (Maxime Dénès)
- 11:00 Break
- 11:15 Reality check: unmaintained source code, what do we do with it? (Enrico Tassi)
- 11:45 The State of the State (Emilio Jesús Gallego Arias)
- 12:15 Lunch
- 13:30 Technical work in small groups (Enrico proposes: (ssr)matching + setoid rewrite)
- 15:00 New horizons for tactics (Maxime Dénès)
- 16:00 SSReflect 2.0 (Enrico Tassi)
- 9:00 Coffee
- 10:00 Progress Report on the API front (Matej Košík)
- 10:30 Travis (Emilio Jesús Gallego Arias)
- 11:00 Break
- 11:15 Artifact evaluation and formal proofs (Assia Mahboubi)
- 11:35 Streamlining the CEP process (Enrico Tassi)
- 11:55 Porting the reference manual to Sphinx (Maxime Dénès)
- 12:15 Lunch
- Afternoon: technical work in small groups. (Matthieu suggests a group on evar_source/evar_kind/evar extra and merging at evar-evar problems)
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.