[TYPES/announce] CfPart: School on Formalization of Mathematics (March 12-16, 2012, Sophia Antipolis, France)

[Yves Bertot]

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

http://www-sop.inria.fr/manifestations/MapSpringSchool/ 
Application deadline: February 27th, 2012 

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 aim of this school is to give mathematicians and mathematically 
inclined researchers the keys to the Coq system and the Mathematical 
Components library. The topics covered are: 

Formal proof techniques 
Structuring libraries 
Encoding of common mathematical structures 
Formal description of algorithms 
An overview of advanced projects: 
* The odd order theorem 
* Constructive algebraic topology 
* Kepler's conjecture, 
* Computational analysis, 
* Foundational investigations. 

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 exercises. 

Speakers 

The current list of speakers is: 

Georges Gonthier (Microsoft Research) 
Thomas C. Hales (University of Pittsburgh) 
Julio Rubio (Universidad de La Rioja) 
Bas Spitters (Radboud Universiteit, Nijmegen) 
Vladimir Voevodsky (Institute for advanced study, Princeton) 
Yves Bertot (Inria) 
Assia Mahboubi (Inria) 
Laurence Rideau (Inria) 
Enrico Tassi (MSR-Inria common laboratory) 
Laurent Théry (Inria) 

Registration 

The registration fee is 320 Euros. A registration form is available on the web site 

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


Location 

The school will take place at Inria's Sophia Antipolis research center. This center is 
located 20 mn by bus from the city Antibes on the Mediterranean sea, nearby 
Nice's international airport, with a variety of hotels at a walking distance. Advice for 
accomodation is provided on the web page. 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20111128/454d7211/attachment-0001.html>