skip to content

UniMath - its present and its future.

Presented by: 
Vladimir Voevodsky
Monday 10th July 2017 - 11:30 to 12:30
INI Seminar Room 1
UniMath refers to several things. It is a
univalent foundation of mathematics. It is the subset of Coq in which this
foundation is currently implemented and it is a library of formalized
mathematics written using this implementation. My talk will be mostly about the
library. I will give examples of problems whose constructions have been
recently formalized in the UniMath as study problems by graduate students. I
will give an example of a more complex problem whose construction has been
recently formalized as a part of a paper accepted to a conference proceedings.
Finally, I will outline a direction for the future development of the UniMath
that requires constructions to considerably more complex problems that can only
be stated in the univalent type theory and, as far as I know, have never been
solved either formally or informally.
The video for this talk should appear here if JavaScript is enabled.
If it doesn't, something may have gone wrong with our embedded player.
We'll get it fixed as soon as possible.
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons