School
The Mathematical Components school will take place on Monday 5th December 2022 to Friday 9th.
Flash info:
- Link to installers
- Video of the first lecture is online
- Video of the fourth lecture is online
5th
- 09:00 - 10:00 introduction to SSReflect and the MathComp library (Enrico Tassi)
Tactics, notations, principles of Small Scale Reflection and the Mathematical Components library
online lesson | lesson1.v | video - 10:30 - 12:00 exercise session 1
SSR cheat sheet | exercise online | exercise1.v | solutions - 12:00 - 14:00 lunch
- 14:00 - 15:00 arithmetics (Laurent Thery)
Order, division, primality, permutations
online lesson | lesson2.v - 15:30 - 17:00 exercise session 2
exercise online | exercise2.v | solutions
6th
- 09:00 - 10:00 finite types and big operators (Yves Bertot)
Handling notions of finiteness and finitely iterated operations
online lesson | lesson3.v -
10:30 - 12:00 exercise session 3
exercise online | exercise3.v | solutions - 12:00 - 14:00 lunch
- 14:00 - 15:00 SSReflect and its idioms (Enrico Tassi)
Advanced features of the proof language
online lesson | lesson4.v | video - 15:30 - 17:00 exercise session 4
exercise online | exercise4.v | solutions
Workshop
See the dedicated page
8th
- 09:00 - 10:00 the algebra library (Cyril Cohen)
Interfaces and instances of the algebra library; notations and theorems about rings online lesson | lesson5.v - 10:30 - 12:00 exercise session 5
exercise online | exercise5.v | solutions - 12:00 - 14:00 lunch
- 14:00 - 15:00 polynomials (Laurence Rideau)
Polynomials: data structure, algorithms and proofs
online lesson | lesson6.v - 15:30 - 17:00 exercise session 6
exercise online | exercise6.v | solutions
9th
- 09:00 - 10:00 matrix library (Cyril Cohen)
Matrices and related algorithms
online lesson | lesson7.v - 10:30 - 12:00 exercise session 7
exercise online | exercise7.v | solutions - 12:00 - 14:00 lunch
- 14:00 - 15:00 tooling and automation (Kazuhiko Sakaguchi)
Reflection based automation
online lesson | lesson8.v - 15:30 - 17:00 exercise session 8
exercise online | exercise8.v | solutions