Home
Invited speakers
- Thorsten Altenkirch (University of Nottingham, UK)
- Andrea Asperti (University of Bologna, Italy)
- Ulrich Berger (Swansea University, UK)
- Gilles Dowek (INRIA, Paris, France)
- Peter Dybjer (Chalmers University of Technology, Göteborg, Sweden)
- William M. Farmer (McMaster University, Hamilton, Canada)
- Herman Geuvers (Radboud University Nijmegen, The Netherlands)
- Georges Gonthier (Microsoft Research, Cambridge, UK)
- Hugo Herbelin (INRIA, Paris, France)
- Fairouz Kamareddine (Heriot-Watt University, Edinburgh, UK)
- Michael Kohlhase (Jacobs University, Bremen, Germany)
- Artur Kornilowicz (University of Bialystok, Poland)
- Zhaohui Luo (Royal Holloway, University of London, UK)
- Erik Palmgren (Stockholm University, Sweden)
- Peter Schuster (University of Leeds, UK)
- Helmut Schwichtenberg (Ludwig Maximilians University, Munich, Germany)
|
Photo by Giovanni Sambin
|
Photo by Giovanni Sambin
|
Description
Nowadays, every mathematician who is going to use an interactive theorem prover is asked to fill the gap between the standard mathematical practice and the formal language understood by the system.
This comprises, but is by no means restricted to, the translation of extensional mathematical languages and theories into intensional foundations like type theory.
The time is ripe for a renewed foundational theory that takes into account different languages and theories and explicitly describes their mutual connections.
Such a foundational theory should provide more automation for translating mathematical texts into lower level languages.
At least in principle, the task of implementing a specific piece of Mathematics would then rely not on the mathematician's programming skills, but on the particular design of the foundational theory instead.
To coin a phrase, not implementations of theories, but a theory of implementation.
The aim of the workshop is to collect outstanding experts, both from Computer Science and from Mathematics, for discussing possible foundations suitable to facilitate such an integration between informal Mathematics and its interactive formalization.
In particular, we would like to focus on the theoretical, logical tools needed to meet this goal.
As a case study, we would like to test Maietti-Sambin's proposal of a minimalist two-level foundation that accommodates a high level extensional language with proof irrelevance and a low level constructive type theory.
|
|
