|
Georges Gonthier
Microsoft Research, UK
Software engineering for mathematics
Friday, August 23
09:30-10:30, Column Hall
Since Turing, we have wanted to use computers to store, process, and check mathematics. However even with the assistance of modern software tools, the formalization of research-level mathematics remains a daunting task, not least because of the talent with which working mathematicians combine diverse theories to achieve their ends. By drawing on tools and techniques from type theory, language design, and software engineering we captured enough of these practices to formalize the proof of the Odd Order theorem, a landmark result in Group Theory, which ultimately lead to the monumental Classification of finite simple groups. This involved recasting the software component concept in the setting of higher-order, higher-kinded Type Theory to create a library of mathematical components covering most of the undergraduate Algebra and graduate Group Theory syllabus. This library then allowed us to write a formal proof comparable in size and abstraction level to the 250-page textbook proof of the Odd Order theorem.
About the Speaker.
Georges Gonthier is a Principal Researcher at Microsoft Research Cambridge, which he joined in 2003, after 13 year in France at Inria. Dr. Gonthier has worked on the Esterel reactive programming language, optimal computation of functional programs, formal verification of concurrent memory management, the join calculus model of concurrency and security, concurrency analysis of the Ariane 5 flight software, and a fully computer-checked proof of the famous Four Colour Theorem. He now heads the Mathematical Components project at the MSR Inria Joint Center, which recently completed the formalization of the Odd Order theorem, the landmark result that ultimately lead to the Classification of Finite Simple Groups. Dr. Gonthier was awarded the EADS Grand Prize in Computer Science in 2011.
|