Autumn school "Proof and Computation", 13th and 14th September 2021
An international autumn school "Proof and Computation" will be held virtually from 13th to 14th September 2021. Its aim is to bring together young researchers in the field of Foundations of Mathematics, Computer Science and Philosophy. Previous autumn schools in this series were PC19 in Herrsching, PC18 in Fischbachau (Aurachhof), PC17, PC16.
Scope
- Predicative Foundations
- Constructive Mathematics and Type Theory
- Computation in Higher Types
- Extraction of Programs from Proofs
Talks
- Liron Cohen: Effectful Proving (and Disproving)
- David Corfield: Modal Type Theories
- Grigory Devadze: Computer-certified proofs for control theoretic aspects and program extraction
- Dominik Kirst: Formalising Metamathematics in Constructive Type Theory
- Klaus Mainzer: Proof and Computation: Perspectives of Mathematics, Computer Science, and Philosophy
- Antonio Piccolomini d'Aragona: Epistemic grounding. Semantics and calculi based on Prawitz's theory of grounds
- Sebastian Posur: On free abelian categories for theorem proving
- Florian Steinberg: Continuity, computability and discreteness
- Holger Thies: Complexity Theory in Analysis with Applications to Differential Equations
Schedule
- 13. September, 14-15 Mainzer
- 13. September, 15-16 Corfield
- 13. September, 16-17 Cohen
- 14. September, 09-10 Thies
- 14. September, 10-11 Steinberg
- 14. September, 11-12 Piccolomini
- 14. September, 14-15 Devadze
- 14. September, 15-16 Posur
- 14. September, 16-17 Kirst
Registration
If you are interested in participating please send an email to Nils Köpp (koepp[at]math.lmu.de).
Public screening in Augsburg
For participants interested in meeting in person instead of online, there will be an organized public screening at the University of Augsburg. In addition to following the talks together, there will be informal exercise and discussion sessions and a conference dinner. The hope is to recreate a small part of the unique atmosphere of previous installments of Proof and Computation. Free simple accomodation is provided, but there is no travel reimbursement. The meeting starts on Monday and ends on either Tuesday or Wednesday, depending on demand. To participate in Augsburg, a mandatory but nonbinding registration with the local organizer Ingo Blechschmidt is required. You need to be vaccinated, recovered or tested.
Abstracts
- David Corfield: Modal Type Theories. Modal logic has a long history in philosophy stretching back to C. I. Lewis's work early in the last century. Over recent decades many researchers have looked to develop modal variants of type theory, with applications extending from computer science to mathematical physics. In this talk we will consider the ways in which philosophers might make use of modal types.
- Dominik Kirst: Formalising Metamathematics in Constructive Type Theory. In this talk, I outline our investigation of metamathematical results using constructive type theory as implemented in the Coq proof assistant. The first part of the talk introduces the synthetic approach to computability based on the fact that all functions definable in a constructive meta-theory are computable, hence avoiding reference to formal models of computation such as Turing machines. The second part demonstrates how this approach can be applied to some decision problems in first-order logic: validity and provability (the original Entscheidungsproblem), finite satisfiability (Trakhtenbrot's theorem), and entailment in first-order axiom systems such as PA and ZF (yielding incompleteness of PA and ZF). Complementing these negative results, I'll also briefly discuss the constructive analysis of the completeness of first-order logic in our setting.
- Klaus Mainzer: 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 AI-technology. References: K. Mainzer, The Digital and the Real World. Computational Foundations of Mathematics, Science, Technology, and Philosophy, World Scientific Singapore 2018; K. Mainzer/P. Schuster/H. Schwichtenberg (Eds.), Proof and Computation. Digitization in Mathematics, Computer Science, and Philosophy, World Scientific Singapore 2018; K. Mainzer/P. Schuster/H. Schwichtenberg (Eds.), Proof and Computation II. From Proof Theory and Univalent Mathematics to Program Extraction and Verification, World Scientific Singapore 2021.
- Antonio Piccolomini d'Aragona: Epistemic grounding. Semantics and calculi based on Prawitz's theory of grounds. Building upon Prawitz's *theory of grounds*, I propose a formal framework for epistemic grounding. First, I outline a "universe" of typed epistemic grounds over atomic bases over first-order background type-languages. Then, I introduce formal languages of grounding and define over them denotation functions that map terms onto epistemic grounds. I explore some properties of this denotational semantics - e.g. correctness, canonical closure, primitive/non-primitive extensions of a language of grounding etc. Finally, I define formal systems over languages of grounding for proving relevant facts about epistemic grounding - e.g. the given term has the given type, the given terms are computationally equivalent, computation instructions for evaluating terms to canonical forms are convergent etc. I prove that each system is sound and enjoys a normalisation property, and I investigate some consequences of these results.
- Sebastian Posur: On free abelian categories for theorem proving. Computing explicitly within a free mathematical object can be interpreted as theorem proving. In this talk, we discuss the constructiveness of free abelian categories. A very concrete description of free abelian categories was given by Murray Adelman, and we demonstrate how his description can be employed to validate homological lemmata like the Snake lemma computationally.
- Holger Thies: Complexity Theory in Analysis with Applications to Differential Equations. Computable analysis is an extension of classical computability theory to computations with uncountable entities such as the real numbers. The rigorous study of computational complexity of real functions based on this model was initiated by Ko and Friedman. The theory can be extended to more general spaces using the framework of representations. In this talk we introduce the necessary notions from computable analysis and real number complexity theory and present some applications to operators in analysis, in particular problems related to solving ordinary and partial differential equations. If time allows we also explore some connections to constructive mathematics and formalization in proof assistants.
The workshop is supported by the
Udo Keller Stiftung (Hamburg) and the CID (Computing with Infinite
Data) programme of the European Commission.
Last change: 10. September 2021