-
Notifications
You must be signed in to change notification settings - Fork 62
FormaSys kick‐off meeting topics
- link between monae and mca
- ODE solving and integration of MCA in his dev
- Mathcomp without deceq or with various levels of classicality
- Porting the inverted pendulum
- Complex analysis and type inference issues
- HB missing commands -> change of structures
- QBS
- using trocq to change datatypes, e.g. reals or tuples
- HB change of structures
- Remove articifial dependencies in classical axioms
- HB improvements
- refinements of trajectories
- proof that:
- the paths do not have collisions
- Dijstra algorithm
- refinements with monads
- complex analysis
- manifolds
- HB change of subject by application
- available on Friday morning to formalize stuff
- formalization of probabilistic semantics
- long term goals: prove compiler passes
- equivalence between kernel based and density based semantics
- QBS and ωPAP spaces
- Question: mathcomp school collocated with FormaSys?
- Applications of relational parametricity
- re-implementation of the internals of algebra tactics package: polynomials with commutative and non-commutative variables
- cache the results of conversion
Participants:
- Holger
- Yoshihiro
- Quentin
- Reynald
- (Cyril)
Topics:
- ODE solving and integration with MCA
Participants
- Jacques
- Lucie
- Yves
- Takafumi
- (Kazuhiko)
- (Cyril)
Topics:
- Trocq for refinements to monadic programs
Topics: Complex Analysis
Participants:
- Cyril (talk)
- Kazuhiko
- Reynald
- Jacques
- Lucie
- Takafumi
Topics:
- Trocq for mathcomp and MCA
Schedule:
Participants:
- Holger
- Yoshihiro
- Quentin
- (Cyril)
Goals:
- Algorithm refinement using naive functions
- Data refinements to substitute naive functions with projections of a record.
- Example: Fibonacci
Schedule:
Participants:
- Jacques
- Lucie
- Yves
- Takafumi
- (Kazuhiko)
- (Cyril)
Goal:
- change reals to canonical reals (see categoricity)[https://github.com/rocq-community/fourcolor/tree/master/theories/reals]
- row vectors to tuples
- polynomials of bounded size ⊂ polynomials
Schedule:
Participants:
- Cyril (talk)
- Kazuhiko
- Reynald
- Jacques
- Lucie
- Takafumi
Time constraints: from Wednesday
Participants:
- Kazuhiko
- Quentin
- Enrico
- Reynald
- (Cyril)
Just wants to see the results:
- Takafumi (PR review)
Program:
- State of affairs
Goal: deprecate mixin and factory keywords, provide one go structure declaration
- (Cyril)
- Enrico
- Lucie
Goals:
-
FAQ and doc of current users
-
Rethink how to infer alternative instances
-
Jacques
-
Takafumi
-
Reynald
-
(Cyril)
-
Kazuhiko
- (Reynald)
- (Cyril)
TODO: Schedule a meeting with Marie
Participants:
- Reynald
- Takafumi
- Quentin
- (Cyril)
Subtopic:
- Manifolds
Goals: comment on PR
Remark: better fitted for MC sharing days
TBD
- Takafumi
- Reynald
- (Cyril)
Goal:
-
making decidable equality optional
-
adding various degrees of classicality (e.g. choice)
-
(Cyril)
-
Holger
-
(Quentin)
-
(Takafumi)
Time constraints: Friday morning
- Guillaume
- Reynald
- Yoshihiro
- Takafumi
- (Cyril)
- Cyril
- Reynald
- Takafumi
- Quentin
- Cyril
- Pierre
- Reynald
- Kazuhiko
- Enrico
- Quentin
- Cyril
- Reynald
- Yves
- Takafumi (especially the convexity part)
Important information is that the proof of correctness for the vertical cell decomposition algorithm is now complete. At this stage, it should be easy to show the two following facts:
- every segment where both extremities are strictly inside the same cell is safe
- every triangle with one point in one cell and one point in an adjacent cell, and the two segments intersecting with the same door is safe.
Refinements with imperative features.
- Pierre
- Kazuhiko
- I can describe the recent version of A bargain for mergesorts (NB: the publicly-available preprint is outdated), which exploits a case where parametricity implies naturality (which is also an instance of free theorems) and the fact that parametricity implies induction principles on Church-encoded datatypes (which is perhaps related to the derive plugin of Rocq-Elpi).
- I plan to establish RocqEAL-style refinements for commutative and non-commutative polynomials in
monalg.vof multinomials, derive a reflexive decision procedure for non-commutative (semi)algebras over commutative (semi)rings (by exploiting the fact that mixed commutative and non-commutative polynomials are isomorphic to non-commutative polynomials over commutative polynomials), and later extend it to non-square matrices over commutative (semi)rings using untyping theorems
- Enrico
The idea is to reduce the calls of coq.unify-eq (and thus readback). It shouldn't be hard to implement, but the challenge would be not compromising the readability and maintainability of reification procedures, as we need to pass around the state. There is a related open issue of Algebra Tactics.
- Kazuhiko
- Enrico
- how does this compare to tabling?
- KS: The advantage of union-find is that it computes the symmetric and transitive closure of the set of known equations. Perhaps, we should try tabling first since it 1) looks like a lightweight yet very effective approach and 2) has the advantage that it automatically caches disequations.
- how does this compare to tabling?
- Jacques
- Reynald
- Cyril
- Takafumi
- Cyril (whole week)
- Pierre (Wed, Thu, Fri)
- Yves (Mon, Tue, Wed)
- Kazuhiko (whole week)
- Reynald (whole week)
- Holger (whole week)
- Enrico (mon, tue, wed)
- Jacques (whole week)
- Quentin (whole week)
- Takafumi (whole week)