Skip to content

2018 12 12 Meeting

Damien Rouhling edited this page Dec 13, 2018 · 2 revisions

Initial agenda of the meeting:

  • Advances on the paper
  • Announce mathcomp-analysis on mathcomp dev mailing list?
  • What is everyone doing?
  • PR statuses

Participants

  • Reynald Affeldt
  • Cyril Cohen
  • Marie Kerjean
  • Assia Mahboubi
  • Laurence Rideau
  • Damien Rouhling
  • Pierre-Yves Strub

Summary

Next Meeting

  • Cyril will open a poll for a meeting in January

Communication

Web communication

  • We should have a visible website
  • We should advertise the library on Coq's channels
  • Cyril opened a Gitter channel here

Paper

  • Back to the tension between lack of space and lack of advertisement: we will write a journal paper as if it was for LMCS (better delays than MSCS) and then decide if we extract a part for a conference or if instead we present the library in workshops
  • Goal: clearly explain our formalization methodology
  • Target audience:
    • "math researchers" (typically people on Lean's Zulip channel)
    • people from program certification (e.g. measure theory is required for the certification of probabilistic programs)
    • people interested in the proof of numerical and symbolic computer systems

Misc.

  • To convince people, the library should have access to an adapted version of Interval and its dependencies
  • We should get in touch with Silvain Rideau about ultra-filters
  • Also true for mathcomp: we are not small scale extremists! We should make it clear that using tactics such as lra and ring is perfectly fine with us.

Prop vs bool

  • Assia informed us of discussions about sProp (elements of P : sProp are convertible)
  • We discussed the possibility of replacing bool/Prop with sProp + a decidable class