Next LIRMM Colloquium – Gérard Berry – 2 June 2022

On Thursday 2 June, from 2 pm, we will have the pleasure of welcoming Gérard Berry, an eminent computer scientist, former student of the École polytechnique, general engineer of the Corps des Mines, member of the Académie des sciences, the Académie des technologies and the Academia Europaea. He will come to speak to us about formal logics with applications in the scientific and industrial worlds.
Come to our Campus for this next colloquium, in the St Priest amphitheatre, to share this moment of science and conviviality.
Biography: https://www.college-de-france.fr/site/gerard-berry/
Subject: From formal logics to applications in the scientific and industrial worlds
Abstract: For a long time, formal logic was considered only as a foundation of mathematics, not really useful in practice. But its progress has led in the last 30 years to entirely new applications, of great size and importance. We will detail two quite different cases: finite logics such as pure Boolean calculus and Boolean modulo decidable theories, and the use of proof assistants. For finite logics, Boolean calculus, which was thought to be insoluble even at medium scales, has undergone two revolutions. First, that of binary decision diagrams (BDDs), then that of Boolean Satisfaction Analysis (SAT), with applications ranging from making Sudoku trivial to systematically checking key properties of electronic circuit designs or solving combinatorial problems in number theory. Then the extension of SAT to decidable theories (SMT) led to a wider spectrum of applications, ranging from the verification of safety-critical applications to the study of certain biological systems. In the broader field of higher-order logics, proof assistants such as HOL, Isabelle, Coq and Lean now allow formal proofs of large mathematical theorems (4-colour, Feit-Thompson, Kepler, etc.), but also important practical computer applications such as formal verification of the CompCert C compiler or of operating system cores, undertakings that were unthinkable until recently. We will conclude with some thoughts on the convergence of finite methods and proof assistants, which will be necessary in the future.