Mainzer K. Proof and Computation...2018

Textbook in PDF format

Today’s debate about safety and reliability of data and algorithms is very similar to the logical-mathematical debate on foundations in the early 20th century — today, however, with grave consequences for technology and economy. The key to the solution of these problems is to be found in the logical foundations of mathematics and computer science themselves, the current development of which leads to new joint research methods and perspectives in mathematics and computer science.
In this vein, an international autumn school “Proof and Computation” was held from 3rd to 8th October 2016 at Aurachhof in Fischbachau near Munich. Its aim was to gather together young researchers active in the foundations of mathematics, computer science, and philosophy. There was the opportunity to form ad-hoc groups working on specific projects, but also to discuss in more general terms the vision of extracting correct programs from proofs. The participants worked on predicative foundations, constructive mathematics and type theory, computation in higher types, extraction of programs from proofs, and algorithmic aspects in financial mathematics.
Lectures were given by Laura Crosilla on predicativity, Hajime Ishihara on constructive analysis, Stan Wainer on computability, Masahiko Sato on lambda calculus, Kenji Miyamoto on program extraction from proofs, Andreas Abel on Agda, and Josef Berger on algorithmic aspects of financial mathematics.
Preface
Proof and Computation
Klaus Mainzer
Constructive Convex Programming
Josef Berger and Gregor Svindland
Exploring Predicativity
Laura Crosilla
Constructive Functional Analysis: An Introduction
Hajime Ishihara
Program Extraction
Kenji Miyamoto
The Data Structures of the Lambda Terms
Masahiko Sato
Provable (and Unprovable) Computability
Stanley S. Wainer
Introduction to Minlog
Franziskus Wiesnet
List of Contributors