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

Attending (please complete)

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