CoqWG20160928 - coq/coq GitHub Wiki

Organization

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.

Schedule

Videos of some of the talks are available here: https://www.youtube.com/watch?v=JCdUDB_2VwE

28/09/2016

  • 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

29/09/2016

  • 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

⚠️ **GitHub.com Fallback** ⚠️