FormaSys kick‐off meeting topics

Topics and people interested

Complex analysis

• Cyril

Drafting HB missing subject-change related commands

• Cyril
• Pierre

Porting the inverted pendulum to mathcomp 2

• Cyril

Proving trajectories correct

• Yves

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.

LRA without Stdlib

• Pierre

Parametricity and its consequences: free theorems, refinements, and induction principles

• Kazuhiko
  • I can describe the recent version of A bargain for mergesorts.
  • I plan to establish RocqEAL-style refinements for commutative and non-commutative polynomials in monalg.v of multinomials, derive a reflexive decision procedure for non-commutative (semi)algebras over commutative (semi)rings, and later extend it to non-square matrices over commutative (semi)rings using untyping theorems.

Attending (please complete)

• Cyril (whole week)
• Pierre (Wed, Thu, Fri)
• Yves (?)
• Kazuhiko (whole week)