Proof Assistants and Their Applications in Mathematics and Computer Science

Since their beginnings in the 1960s, proof assistants (also called interactive theorem provers) have grown to become essential tools to establish the correctness of hardware and software and to computerize mathematical theories. Specifically, proof assistants are computer programs that help users formally describe mathematical statements and proofs, making them amenable to mechanical checking. Today these programs are used to verify microprocessor designs, operating systems, compilers, and cryptographic protocols—as well as landmark results in mathematics such as the odd order theorem in finite group theory and the Kepler conjecture about sphere packing. Contemporary proof assistants rely on a sophisticated interaction between theoretical investigations in metamathematics and the efficient implementation of a portfolio of algorithms. This volume is designed to be an introduction to these fascinating topics. Topics and features: - Guides the reader through decades of research into designing and using proof assistants - Provides convenient, appropriate citations for the proof assistants’ underlying logical formalisms, architectures, and applications - Grounds the exposition by starting with key topics that are treated across all relevant logical foundations and systems, in a system-agnostic and logic-ecumenical way - Builds on those core topics in the second part, which is dedicated to a gallery of achievements in mathematics and computer science This unique volume is designed to serve as a useful resource both for early or more established researchers in interactive theorem proving and for researchers in mathematics, computer science, and philosophy—as well as for engineers who want to use proof assistants. The volume is edited by Jasmin Blanchette, professor at the Ludwig-Maximilians-Universität München, Germany, and Assia Mahboubi, senior researcher at Inria, France, and endowed professor at the Vrije Universiteit Amsterdam, the Netherlands.