CoqWG20170306 - coq/coq GitHub Wiki
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)