International Spring School on

FORMALIZATION OF MATHEMATICS

(MAP 2012)

March, 12-16, 2012, Sophia Antipolis,France

• Home
• Program
• Registration
• Venue
• Accomodation
• Contact

Program

Monday 12	Tuesday 13	Wednesday 14	Thursday 15	Friday 16
8:45-10:00 Registration	9:00-9:40 lecture: Changing points of view (P.-Y. Strub)	9:00-9:40  lecture: A first tour of the library (L. Rideau)	9:00-9:40  lecture:  Advanced topic on finite groups (E. Tassi)	9:00-10:00  Invited lecture: Designing a universe polymorphic type system (Vladimir Voevodsky)
10:00-10:40 lecture: Introduction to formalizing mathematics (Y. Bertot)
10:40-12:00 laboratory session	9:40-11:30 laboratory session	9:40-11:30 laboratory session	9:40-11:30 laboratory session	10:30-11:30 Invited lecture: From computational analysis to thoughts about analysis in HoTT (Bas Spitters)
12:00-12:40 lecture: Logics and basic tactics (L. Rideau)	11:30-12:10 lecture: More advanced tactics (E. Tassi)	11:30-12:10 lecture: Big operations (Y. Bertot)	11:30-12:10 lecture: Advanced topic on the Cayley-Hamilton theorem (P.-Y. Strub)	12:00-13:30 Lunch
12:40-13:30 Lunch	12:10-13:30 Lunch	12:10-13:30 Lunch	12:10-13:30 Lunch	13:30-14:30 Invited lecture: Lessons from the Flyspeck Formalization Project (Thomas Hales)
13:30-15:20 laboratory session	13:30-15:20 laboratory session	13:30-15:20 laboratory session	13:30-15:20 laboratory session	15:00-16:00 Invited lecture: Design and architecture of the background theories for the Odd Order Theorem (Georges Gonthier)
15:20-16:00 lecture: Programming in Coq (L. Théry)	15:20-16:00 lecture: Canonical Structures (A. Mahboubi)	15:20-16:00 lecture: The algebraic library (A. Mahboubi)	15:20-16:00 lecture: Advanced topic on linear algebra (L. Théry)
16:00-18:00 laboratory session	16:00-18:00 laboratory session	16:00-18:00 laboratory session	16:00-17:30 laboratory session
		Gala Dinner Restaurant Bijou Plage	17:30-18:30 Invited lecture: Formalization of Mathematics: why Algebraic Topology? Julio Rubio