UniMath - its present and its future.

Add to your list(s) Download to your calendar using vCal

• Vladimir Voevodsky (Institute for Advanced Study, Princeton)
• Monday 10 July 2017, 11:30-12:30
• Seminar Room 1, Newton Institute.

If you have a question about this talk, please contact INI IT.

BPRW01 - Computer-aided mathematical proof

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.

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

• All CMS events
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• Seminar Room 1, Newton Institute
• bld31

Note that ex-directory lists are not shown.