Participants

• Xavier Allamigeon
• Yves Bertot
• Cyril Cohen
• Maxime Dénès
• Emilio Gallego Arias
• Assia Mahboubi
• Laurence Rideau
• Damien Rouhling
• Enrico Tassi
• Laurent Théry

Location

Fermat F102, Inria Sophia Antipolis
2004 route des Lucioles, 06902 Sophia Antipolis
Inria or Templier bus stops

https://goo.gl/maps/8YJtHAqpkm92

Tentative Program

November 21st, 2PM - 5PM

• Infrastructure and organization of the development of the libraries

November 22nd, 10AM - 5PM

• Documentation
• Visibility and teaching
• Community
• Future plans for the libraries

Suggestions for topics

• Downstream users and change management [how should the many users of math-comp be managed] (Emilio)
• Role of different theorem provers with mathcomp derivatives [dedukti / easycrypt] (Emilio)
• Solicit offers and requests for future formalization topics (Georges)
• Survey users about the organization of the library: granularity, naming policies... (Georges)
• Survey users about the documentation: what is missing in the existing content, what are they ready to provide with their own new contributions (Georges)
• How to get a feet in Software foundations, and the PL community of Coq users. (Enrico)
• How to improve visibility: teaching material, website, gallery, etc. (Assia)

Minutes

The minutes of the meeting are here.