[logic-ml] September 1st - research talks by Yves Bertot, Pierre Casteran and Assia Mahboubi at University of Tokyo

[Jacques Garrigue]

名古屋大学のGarrigueです。

来る月曜日（9月1日）Coqの専門家三人による講演会を東京大学本郷キャンパスで開きます。
皆様をお待ちしています。

On Monday, September 1st, three of the lecturers of the Shonan School on Coq will give talks
at the University of Tokyo (Hongo Campus). We are waiting for you.

David Nowak and Jacques Garrigue

——
Date: September 1st, 2014 (Monday)
Time: 14:00 - 16:30
Place: room 007, Faculty of Science Bldg. 7, Hongo Campus, The University of Tokyo
URL: http://jfli.cnrs.fr/index.php/special-jfli-seminar-coq

On the occasion of the NII Shonan School on Coq, JFLI organizes a special seminar on formal proofs in Coq with talks by three of the school's lecturers: Yves Bertot and Pierre Castéran (two of the 2013 ACM Software System Award laureates) will present some of their recent work. And Assia Mahboubi will present the formalization in Coq of the Feit-Thompson theorem (a.k.a. odd order theorem) achieved in 2012 under the direction of Georges Gonthier.

14:00 - 14:45: Yves Bertot

PI, Arithmetic geometric means, and formal verification in Coq using Coquelicot

In an experiment spanning over several months, we formally verified an abstract model of an algorithm to compute PI to a large number of digits using arithmetic geometric means.

The proof that we used relies on a few non elementary aspects, like reasoning about improper integrals or deriving under the integral sign, and revolved around manipulating real numbers. This is why we call this an abstract model.

Then we used the recent extension of Coq with native compilation to test the algorithm on a concrete setting, using large integers. As a result we are able to compute in the order of a million of decimals of PI within the theorem prover.  We also proved the correctness of this implementation.  This involves bounding the cumulated errors brought by multiplication, division, and square-root during fixed-point multiplications.

This work benefits from the overall quality of the Coq system and the following recent contributions: the coquelicot library by Boldo & al., the psatzl tactic by F. Besson, and native compilation by M. Dénès.

14:45 - 15:30: Pierre Castéran

 Formal Proofs of Local Computation Systems

Local Computations (LC) are an abstract model for distributed algorithms based on message passing. Each processor can only interact with its neighbours. The current configuration of a static network is represented as a labelling of the vertices and edges of a graph.

This model allows us to study the importance of such hypotheses on the network's behaviour such as synchrony, anonymity, initial knowledge of the processors. Algorithms are splitted into several classes, according to the precise way in which every processor interacts with its neighbours.

LoCo is a formalization of LC in the Coq proof assistant. This library allows us to simulate algorithms, to prove their correctness, and also to prove more abstract results:

		• Impossibility results, i.e., proving that some task is not realisable within a given subclass of LC;
		• Certified transformations, that are functions that map one or several proved algorithms into a new proved algorithm;
		• Analysis of some simple random distributed algorithms.
The talk will show how Coq's rich type system and computation rules allowed us to build this library. Perspective of future work will also be discussed.

15:30 - 15:45: break

15:45 - 16:30: Assia Mahboubi

Computer-checked mathematics: a formal proof of the Odd Order theorem

The Odd Order Theorem is a landmark result in finite group theory, famous for its crucial role in the classification of finite simple groups, for the novel methods introduced by its original proof but also for the striking contrast between the simplicity of its statement and the unusual length and complexity of its proof. This talk presents the six-year collaborative work that led to a complete formalization of this theorem, using the Coq proof assistant. The resulting collection of libraries of formalized mathematics covers a wide variety of topics as this proof relies on a sophisticated combination of different flavours of mathematics. These libraries and the underlying methodology can be reused for a wider spectrum of applications. This is a joint work with the Mathematical Components group at the Inria Microsoft Joint Centre.