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).
| Originalsprache | Englisch |
|---|---|
| Titel | Proof and Computation II |
| Untertitel | From Proof Theory and Univalent Mathematics to Program Extraction and Verification |
| Herausgeber (Verlag) | World Scientific Publishing Co. |
| Seiten | 1-32 |
| Seitenumfang | 32 |
| ISBN (elektronisch) | 9789811236488 |
| ISBN (Print) | 9789811236471 |
| DOIs | |
| Publikationsstatus | Veröffentlicht - 1 Jan. 2021 |