Math and Informatics, ever more fruitful interactions

Abstract: The relation between math and algorithmics is very old. In a sense, one can even argue that mathematics was created to show that some already known algorithms worked in all cases and not only on some examples. Church and Turing, creators of the lambda-calculus and computability theory were mathematicians. Informatics was really born later with the introduction of computers, for which mathematicians played an important role. In the 70's, computer algebra was developed, as well as the formal semantics of  programming languages and automatic program analysis techniques. But the cooperation between both sciences has deepened quickly in the last 20 years, with mutual enrichment. We will show this with a variety of examples : the systematic development of randomized and probabilistic algorithms to handle massive data, the use of boolean satisfiability (SAT) systems to solve open problems in number theory, the development of powerful proof assistants for mechanizing large mathematical proofs using rich logics (Feit-Thompson theorem, Kepler conjectures), and finally, the use of the same tools to perform mathematical proofs of the correctness of safety-critical
computerized systems.

Bio: Gérard Berry, a member of the French Académie des Sciences and recipient of the Gold Medal of CNRS in 2014, studied at Ecole Polytechnique and Corps des Mines in Paris. He was Researcher at Ecole des Mines and Inria from 1970 to 2001, Chief Scientist of the Esterel Technologies company from 2001 to 2009, Director of Research at Inria from 2009 to 2012, before being appointed as Full Professor at Collège de France in 2012 on the Algorithms, Programs and Machine Chair; he had previously held there two yearly chairs in 2007-2008 and 2009-2010. He officially retired in 2001. His main scientific contributions concern the formal development of programming languages in relation to mathematical logic, parallel and real-time programming, high-level design of computer circuits and systems, and formal verification of programs and circuits. He is the creator of the Esterel synchronous reactive language. Through his courses, books and conferences, he is also active in the dissemination to a general audience of the new algorithmic way of thinking and acting.