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

## Small ProofsAdd to your list(s) Download to your calendar using vCal - Dan Licata (Wesleyan University)
- Tuesday 11 July 2017, 14:30-15: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 There is an old idea in programming languages that the right way to solve a problem is to (1) design and implement a programming language in which solving the problem is easy, and then (2) write the program in that language. Some applications of homotopy type theory to the formalization of mathematics have this flavor: First, we design a type theory and study its semantics. Then, we use that type theory, including features such as the univalence axiom, higher inductives types, interval objects, and modalities, as a language where it is easy to talk about certain mathematical structures, which enables short formalizations of some theorems. In this talk, I will give a flavor for what this looks like, using examples drawn from homotopy, cubical, and cohesive type theories. I hope to stimulate a discussion about the pros and cons of factoring the formalization of mathematics through the design of new programming languages/logical systems. 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 listsInstitution of Engineering and Technology Public Lectures Centre for Science and Policy Distinguished Lecture Series women@CL Speaker Lunch Series## Other talksSustainability 101: how to frame it, change it and steer it Beyond truth-as-correspondence: realism for realistic people The Anne McLaren Lecture: CRISPR-Cas Gene Editing: Biology, Technology and Ethics Babraham Lecture - The Remote Control of Gene Expression C++ and the Standard Library Enhanced Decision Making in Drug Discovery |