-
Notifications
You must be signed in to change notification settings - Fork 43
2018 12 12 Meeting
Damien Rouhling edited this page Dec 13, 2018
·
2 revisions
- Advances on the paper
- Announce mathcomp-analysis on mathcomp dev mailing list?
- What is everyone doing?
- PR statuses
- Reynald Affeldt
- Cyril Cohen
- Marie Kerjean
- Assia Mahboubi
- Laurence Rideau
- Damien Rouhling
- Pierre-Yves Strub
- Cyril will open a poll for a meeting in January
- We should have a visible website
- We should advertise the library on Coq's channels
- Cyril opened a Gitter channel here
- 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
- 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
andring
is perfectly fine with us.
- Assia informed us of discussions about
sProp
(elements ofP : sProp
are convertible) - We discussed the possibility of replacing
bool
/Prop
withsProp
+ adecidable
class