The theme of the symposium will be "Mathematical formalization and dependent types". Invited speakers include specialists in the implementation or theory of proof assistants, type theory, higher-order category notions, and mathematicians who use these systems to represent proofs on computers. One of the questions addressed will be to what extent the recent rapprochement between the formalism of dependent types and the notions of homotopy and higher-order categories can be relevant to the actual formalization of mathematics.
Symposium