International Spring School on

FORMALIZATION OF MATHEMATICS

(MAP 2012)

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

logo map  
 
 
  logo Inria logo IHP logo microsoft  
 
 
 
 

    Program

    (program at a glance)

    Monday 12

    8:45-10:00 Registration
    10:00-10:40 Lecture:
    Introduction to formalizing mathematics (Y. Bertot)
    slides, examples
    10:40-12:00 Laboratory session
    exercises, solutions
    12:00-12:40
    Lecture:
    Logics and basic tactics (L. Rideau)
    slides
    12:40-13:30 Lunch
    13:30-15:20 Laboratory session
    exercises, solutions
    15:20-16:00 Lecture:
    Programming in Coq (L. Théry)
    slides
    16:00-18:00 Laboratory session
    exercises, solutions

    Tuesday 13

    9:00-9:40 Lecture:
    Changing points of view (P.-Y. Strub)
    slides, examples
    9:40-11:30 Laboratory session
    exercises, solutions
    11:30-12:10
    Lecture:
    More advanced tactics (E. Tassi)
    slides
    12:10-13:30 Lunch
    13:30-15:20 Laboratory session
    exercises, solutions
    15:20-16:00 Lecture:
    Canonical Structures (A. Mahboubi)
    slides
    16:00-18:00 Laboratory session
    exercises, solutions

    Wednesday 14

    9:00-9:40 Lecture:
    A first tour of the library (L. Rideau)
    slides
    9:40-11:30 Laboratory session
    exercises, solutions
    11:30-12:10
    Lecture:
    Big operations (Y. Bertot)
    slides, examples
    12:10-13:30 Lunch
    13:30-15:20 Laboratory session
    exercises, solutions
    15:20-16:00 Lecture:
    The algebraic library (A. Mahboubi)
    slides
    16:00-18:00 Laboratory session
    exercises, solutions
    Advanced exercises On big operations and binomials: counting subsets of odd and even cardinals in any finite set (proposed by J.Grimm).
    On fintypes: Showing that in any group of more than 1 person, there are two persons with the same number of friends (proposed by L. Théry).

      Gala Dinner
    Restaurant Bijou Plage

    Thursday 15

    9:00-9:40 Lecture:
    Advanced topic on finite groups (E. Tassi)
    slides, examples
    9:40-11:30 Laboratory session
    exercises, solutions
    11:30-12:10
    Lecture:
    Advanced topic on the Cayley-Hamilton theorem (P.-Y. Strub)
    slides
    12:10-13:30 Lunch
    13:30-15:20 Laboratory session
    exercises, solutions
    15:20-16:00 Lecture:
    Advanced topic on linear algebra (L. Théry)
    slides
    16:00-17:30 Laboratory session
    exercises, solutions
    17:30-18:30 Invited lecture:
    Formalization of Mathematics: why Algebraic Topology? (Julio Rubio)

    Friday 16

    9:00-10:00 Invited lecture:
    Designing a universe polymorphic type system (Vladimir Voevodsky)
    10:30-11:30 Invited lecture:
    From computational analysis to thoughts about analysis in HoTT (Bas Spitters)
    12:00-13:30 Lunch
    13:30-14:30 Invited lecture:
    Lessons from the Flyspeck Formalization Project (Thomas Hales)
    15:00-16:00 Invited lecture:
    Design and architecture of the background theories for the Odd Order Theorem (Georges Gonthier)

     

    Course contents

    Using computers to state and prove theorems

    • Why trust a computer to check proofs, and what to trust?
    • Typed formulas, quantifications, and logical connectives
    • Using theorems as functions
    • Modeling the mathematical practice of notation abuse

    Principles and practice of goal directed proofs

    • Basic commands for proofs in Coq/Ssreflect
    • Advanced techniques for rewriting an proofs by induction
    • Changing points of views: reflection mechanisms

    A guided tour of the ssreflect library

    • Basic notions: finite sets, numbers, tuples
    • Algebraic notions: polynomials, matrices, vector spaces
    • Structuration principles
    • Illustration on an advanced example

    Lectures on advanced topics

    • Georges Gonthier Design and architecture of the background theories for the Odd Order Theorem

      One of the main objectives of the Odd Order formalization project was to understand how to organize a large working mathematical corpus. The project is nearing completion, with almost all the background and about 80% of the actual proof done, so there is now sufficient experience to judge how well the corpus works. In this talk I will explain and assess some of the trade-offs we made between generality, flexibility, robustness and constructivity, in the design of our theory library, and their impact on usability.

    • Thomas C. Hales Lessons from the Flyspeck Formalization Project

      The Flyspeck project aims to give a formal proof of the statement that the densest packing of congruent balls in Euclidean space is the familiar cannonball arrangement. This project is approaching completion: the 300 page text part of the proof has fewer than 500 lines of informal text left to formalize. This talk will discuss some of the lessons learned.

    • Julio Rubio Formalization of Mathematics: why Algebraic Topology?

      In our days, many parts of mathematics are being studied from the point of view of their formalization by means of mechanized proof assistants. Nevertheless, mathematics is a so wide discipline that most of its areas have not attracted (yet?) the interest of formalization engineers. Why Algebraic Topology, a rather esoteric part of pure mathematics, is being analyzed formally in these last years? We will try to answer this question in the talk, focusing on the computer algebra system called Kenzo, and on our multi-tool approach (using Isabelle/HOL, Coq/SSReflect and ACL2) to formally specify and verify Kenzo.

    • Bas Spitters From computational analysis to thoughts about analysis in HoTT

      Floating point operations are fast, but require continuous effort on the part of the user in order to ensure that the results are correct. This burden can be shifted away from the user by providing a library of exact analysis in which the computer handles the error estimates. We provide a fast implementation of the exact real numbers in the Coq proof assistant. Our implementation improves on an earlier implementation by O'Connor by using type classes to describe an abstract specification of the underlying dense set from which the real numbers are built. In particular, we used dyadic rationals built from Coq's machine integers to obtain a 100 times speed up of the basic operations already. We extend the algebraic hierarchy to capture order on undecidable structures, while it was limited to decidable structures before. This hierarchy, based on type classes, allows us to share theory on the naturals, integers, rationals, dyadics, and reals in a convenient way. Finally, we obtain another dramatic speed-up by avoiding evaluation of termination proofs at runtime. Starting from these developments, I will outline how we could improve this development by using Voevodsky's univalence axiom and forcing technology.

    • Vladimir Voevodsky Designing a universe polymorphic type system

    I will tell about my recent work the goal of which is to design a fully universe polymorphic type system which can be extended with resizing rules.

 
 
webmaster