|Universiteit Faculteit FNWI English version||1 juni 2011, e-mail|
Woensdag 22 juni 2011
AbstractQuite recently, it was discovered that there is a close connection between a certain system of constructive logic and homotopy theory. The system in question, based on Martin-Löf type theory, is used as the basis of automated proof assistants such as Coq, leading to the possibility of computer verified proofs in homotopy theory.
Homotopical intuition and problems also suggest novel extensions of the logical system. In this way, a cross-fertilization of these two formerly unrelated areas of mathematics -- constructive logic and algebraic topology -- is already beginning to take place.
This talk will survey some of these very recent developments.