skip to content

UniMath - its present and its future.

Presented by: 
Vladimir Voevodsky Institute for Advanced Study, Princeton
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.


Presentation Material: 
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons