Отправляет email-рассылки с помощью сервиса Sendsay

Система компьютерной алгебры GAP

Подписаться Бесплатная «Серебряная» новостная рассылка . Временно не выходит ,возобновит выход - нет информации Подписчиков 783 RSS
←   Август 2011   →
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31


За последние 60 дней ни разу не выходила


Сайт рассылки: http://www.gap-system.org/ukrgap/
Открыта: 05-02-2002

Автор
Александр Борисович Коновалов

Статистика

783 подписчиков
0 за неделю
←   Все выпуски   →

Система компьютерной алгебры GAP: International Spring School on FORMALIZATION OF MATHEMATICS



This might be of interest to CIRCA...

International Spring School on FORMALIZATION OF MATHEMATICS
Sophia Antipolis, France
March 12-16, 2012
http://www.inria.fr/sophia/marelle/Map-Spring-School.html

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 practicionner 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-colour 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
* Structuration of libraries
* Encoding of common mathematical structures
* Formal description of algorithms
* An overview of advanced projects:
o The odd order theorem
o Constructive algebraic topology
o Kepler's conjecture,
o Computational analysis,
o 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
exercices.


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 of advanced studies, Princeton University)
* Yves Bertot (INRIA)
* Assia Mahboubi (INRIA)
* Laurence Rideau (INRIA)
* Enrico Tassi (MSR-INRIA common laboratory)
* Laurent The'ry (INRIA)

Registration

The expected registration fee will be between 150 and 200 Euros.
В избранное