This book is for graduate students and researchers, introducing modern foundational research in mathematics, computer science, and philosophy from an interdisciplinary point of view. Its scope includes proof theory, constructive mathematics and type theory, univalent mathematics and point-free approaches to topology, extraction of certified programs from proofs, automated proofs in the automotive industry, as well as the philosophical and historical background of proof theory. By filling the gap between (under-)graduate level textbooks and advanced research papers, the book gives a scholarly account of recent developments and emerging branches of the aforementioned fields.
Contents:
- Proof and Computation: Perspectives for Mathematics, Computer Science, and Philosophy (Klaus Mainzer)
- Conceptions of Proof from Aristotle to Gentzen's Calculi (Stefania Centrone)
- From Intuitionistic Mathematics to Point-Free Topology (Tatsuji Kawai)
- Generalized Spaces for Constructive Algebra (Ingo Blechschmidt)
- A Uniform Characterization of ??-Reflection Over the Fragments of Peano Arithmetic (Anton Freund)
- Formal Topology and Univalent Foundations (Thierry Coquand and Ayberk Tosun)
- An Ad-Hoc Semantics to Study Structural Properties of Types (Marco Benini and Roberta Bonacina)
- The Braga Method: Extracting Certified Algorithms from Complex Recursive Schemes in Coq (Dominique Larchey-Wendling and Jean-François Monin)
- Logic and Verification of Product Configuration in the Automotive Industry (Wolfgang Kuchlin)
Readership: Graduate students, researchers, and professionals in Mathematics and Computer Science.
Key Features:
- The book gathers recent contributions of distinguished experts
- It makes emerging fields accessible to a wider audience, it will appeal to a broad readership with diverse backgrounds in Mathematics, Computer Science, and Philosophy
- It fills a gap between (under-)graduate level textbooks and state-of-the-art research papers
