Paper Info
Title
Software engineering for mathematics (keynote)
Abstract
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.
Year
DOI
Venue
2013
10.1145/2491411.2505429
ESEC / SIGSOFT FSE
Keywords
DocType
Citations 
formal proof,odd order theorem,250-page textbook proof,software component concept,modern software tool,graduate group theory syllabus,higher-kinded type theory,research-level mathematics,group theory,software engineering,theorem proving
Conference
0
PageRank 
References 
Authors
0.34
0
1
Name
Order
Citations
PageRank
Georges Gonthier12275195.06