The Coq mailing list

[bertot <Yves.Bertot AT inria.fr>]

International Spring School
on
FORMALIZATION OF MATHEMATICS
Sophia Antipolis, France
March 12-16, 2012

http://www-sop.inria.fr/manifestations/MapSpringSchool

New: Grants for PhD students covering the full registration fee.

Overview and topics

A growing population of mathematicians, computer scientists, and
engineers use computers to construct and verify proofs of mathematical
results. Among the various approaches to this activity, a fruitful one
relies on interactive theorem proving. When following this approach,
researchers have to use the formal language of a theorem prover to
encode their mathematical knowledge and the proofs they want to
scrutinize. The mathematical knowledge often contains two parts: a
static part describing structures and a dynamic part describing
algorithms. Then proofs are made in a style that is inspired from
usual mathematical practice but often differs enough that it requires
some training. A key ingredient for the mathematical practitioner is
the amount of mathematical knowledge that is already available in the
system's library.

The Coq system is an interactive theorem prover based on Type
Theory. It was recently used to study the proofs of advanced
mathematical results. In particular, it was used to provide a
mechanically verified proof of the four color theorem and it is now
being used in a long term effort, called Mathematical Components to
verify results in group theory, with a specific focus on the odd order
theorem, also known as the Feit-Thompson theorem. These two examples
rely on a structured library that covers various aspects of finite set
theory, group theory, arithmetic, and algebra.

The school's contents will be organized as a balanced schedule between
lectures and laboratory sessions where participants will be invited to
work on their own computer and try their hands on a progressive
collection of exercices.

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 and proofs by induction
- Changing points of views: reflection mechanisms

* A guided tour of the ssreflect library

- Basic notions: numbers, tuples, finite sets
- Algebraic notions: polynomials, abstract algebra, linear algebra
- Structuration principles
- Illustration on an advanced example

Invited lectures
Georges Gonthier (Microsoft Research)
Title to be announced

Thomas C. Hales (University of Pittsburgh)
Lessons from the Flyspeck Formalization Project

Julio Rubio (Universidad de La Rioja)
Formalization of Mathematics: why Algebraic Topology?

Bas Spitters (Radboud Universiteit, Nijmegen)
From computational analysis to thoughts about analysis in HoTT

Vladimir Voevodsky (Institute for advanced study, Princeton)
Designing a universe polymorphic type system

Speakers:

Yves Bertot (INRIA)
Assia Mahboubi (INRIA)
Laurence Rideau (INRIA)
Pierre-Yves Strub (MSR-Inria Joint Centre)
Enrico Tassi (INRIA)
Laurent Théry (INRIA)

Registration

The registration fee is 320€ and includes lunch meals, one evening meal (banquet), and
organization costs. There are a limited number of grants for PhD students,
which cover the full registration fee. A registration form is available on the
web site

http://www-sop.inria.fr/manifestations/MapSpringSchool