Research interests of Helmut Schwichtenberg
Within Mathematical Logic my interests are in proof theory, lambda calculus and recursion theory. In particular I am interested in theoretical and practical studies concerning program extraction from proofs. A tool suitable for this task is the Minlog system under development at the logic group of LMU. It is an interactive proof assistant, designed to help constructing proofs (in minimal logic) on computable functionals and inductively defined predicates. More generally I am interested in applications of logic in computer science. Recent slides:
- A theory of computable functionals, Würzburg 2024
- A theory of computable functionals, Florenz 2024
- A theory of computable functionals, Gothenburg 2022
- Proofs and computation with infinite data, Poznan 2021
- Linear two-sorted constructive arithmetic, Tuebingen 2021
- Logic for exact real arithmetic, St. Petersburg 2021
- Proof and computation with infinite data, Oberwolfach 2020
- Computational content of proofs, Swansea 2019
- Computational content of proofs, CCC Ljubljana 2019
- Equality and extensionality, Bern 2018
- Logic for exact real arithmetic, KMS-DMV Seoul 2018
- Proof and computation, LMU 2018
- Proof theory and computation, Tokyo 2018
- Computational content of the fan theorem for coconvex bars, Kanazawa 2018