• Organization
• Participants
• Talks
• Pierre Courtieu: how to do better than manually naming hypothesis
• Marc Lasson: A new parametricity plugin for the coq proof assistant
• Talking points
• Policy for pull requests: anonymity required? need for at least two reviews? guaranteeing answering delays?
• Library/contribs: editorial board? community managment? licensing? (suggested by B. Spitters)
• Policy: have code that does not require a particular OCaml version to run
• Emit a warning for nested Lemma and the like
• Discussion about nf_constraints + async proofs
• Require inside modules now forbidden
• 8.5 release
• Roadmap