COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > UniMath - its present and its future.

## 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 info@newton.ac.uk. 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
Note that ex-directory lists are not shown. |
## Other listsProteins, Genomes & Computers Empowered Employability Skewness, Heavy Tails, Market Crashes, and Dynamics## Other talksTowards Scale-Free Control of large-scale traffic networks The clinical and biological basis of prostate cancer - from diagnosis to personalised therapy Post-hoc tests, multiple comparisons, contrasts and handling interactions Making Affordable Nuclear Adrian Seminars in Neuroscience - ANNUAL LECTURE Rachel Wilson "Neural correlates of orienting behaviors and latent action biases" Identification of Active Species and Mechanistic Pathways in the Enantioselective Catalysis with 3d Transition Metal Pincer Complexes |