Proof Assistants and Their Applications in Mathematics and Computer Science

Jasmin Blanchette, Assia Mahboubi (Herausgeber)

Buch | Hardcover

X, 390 Seiten

2026
Springer International Publishing (Verlag)
978-3-031-85189-6 (ISBN)

Noch nicht erschienen - erscheint am 12.02.2026
Versandkostenfrei
Auch auf Rechnung

Artikel merken

Proof assistants are computer programs that help users formally describe mathematical statements and proofs, making them amenable to mechanical checking. Today they are used to verify operating systems, compilers, and cryptographic protocols, as well as landmark results in mathematics such as the Feit-Thompson theorem or the Kepler conjecture. Contemporary proof assistants rely on a sophisticated interaction between theoretical investigations in metamathematics and the efficient implementation of a portfolio of algorithms, without which these systems would not usable on a large scale. During the last decade, the use of proof assistants has grown steadily, and they are now at the same time a research topic in its own right and a tool for researchers in other domains. Yet no reference book is available today that covers the entire domain. This book is an introduction and reference for the various topics related to the underlying logical formalisms, architectures, and applications.
The main audience is graduate students entering the field of interactive theorem proving, the secondary audience is more established researchers in computer science, mathematics, and philosophy, as well as practicing engineers, engaged with proof assistants.

Jasmin Blanchette earned his PhD degree in computer science in 2012 from the Technical University of Munich (Germany). He has been active in Germany, France, and the Netherlands, before coming back to Munich. Since 2023, he is professor at the Ludwig-Maximilians-Universität München, where he heads the Chair for Theoretical Computer Science and Theorem Proving. His research focused on using and developing interactive and automatic theorem provers. After graduating in pure mathematics, Assia Mahboubi earned her PhD degree in computer science in 2006 from the University of Nice Sophia Antipolis (France) and her habilitation degree from Nantes University (France). Since 2017, she has been a researcher at the French research institute Inria, conducting research in dependent type theory and formalized mathematics.

Introduction.- Logical Foundations.- Inductive Types and Recursive Functions.- Inductive Predicates.- Coinductive Methods.- Computation.- Elaboration.- Proof Languages.- Proof Automation.- Applications in Computer Science.- Applications in Mathematics.

Erscheint lt. Verlag	12.2.2026
Reihe/Serie	Computer Science Foundations and Applied Logic
Zusatzinfo	X, 390 p. 40 illus.
Verlagsort	Cham
Sprache	englisch
Maße	155 x 235 mm
Themenwelt	Mathematik / Informatik ► Informatik ► Theorie / Studium
	Mathematik / Informatik ► Mathematik ► Allgemeines / Lexika
	Mathematik / Informatik ► Mathematik ► Logik / Mengenlehre
Schlagworte	Computer Science Logic • cryptographic protocols • Inductive Types • metamathematics • Proof Assistants • Proof automation • Proof Languages
ISBN-10	3-031-85189-7 / 3031851897
ISBN-13	978-3-031-85189-6 / 9783031851896
Zustand	Neuware