- Vivi Padova
- Il Bo
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 accomodates a high level extensional language with proof irrelevance and a low level constructive type theory.
Maria Emilia Maietti
Claudio Sacerdoti Coen