Abstract
Computer science, logic and mathematics are connected in the constructions of intuitionistic type theory. In this sense, mathematical constructivism seems to open new avenues of research combining foundations of logic and mathematics with highly topical challenges of IT- and AItechnology. Therefore, after an introduction (chapter 1), we at first consider the development from type theory to univalent mathematics (chapter 2) and from type theory to proof assistants (chapter 3). An application is the verification of circuits with proof assistants (chapter 4). Against this background, chapter 5 highlights the verification of machine learning with AI-methods. The article concludes with practical challenges and societal impact from verification to certification and responsibility (chapter 6).
| Original language | English |
|---|---|
| Title of host publication | Proof and Computation II |
| Subtitle of host publication | From Proof Theory and Univalent Mathematics to Program Extraction and Verification |
| Publisher | World Scientific Publishing Co. |
| Pages | 1-32 |
| Number of pages | 32 |
| ISBN (Electronic) | 9789811236488 |
| ISBN (Print) | 9789811236471 |
| DOIs | |
| State | Published - 1 Jan 2021 |
Fingerprint
Dive into the research topics of 'Proof and Computation: Perspectives for Mathematics, Computer Science, and Philosophy'. Together they form a unique fingerprint.Cite this
- APA
- Author
- BIBTEX
- Harvard
- Standard
- RIS
- Vancouver