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

## Dependent Type TheoryAdd to your list(s) Download to your calendar using vCal - Will Sonnex (Computer Lab)
- Sunday 23 February 2014, 15:00-15:30
- Winstanley Lecture Theatre, Trinity College.
If you have a question about this talk, please contact Mary Fortune. Part of the TMS Symposium What is a mathematical proof as a mathematical object? How do we axiomatize mathematics so that computers can check our proofs, or construct their own (my research)? This talk answers these questions using Dependent Type Theory, and I will show how complex modern mathematics can be built out of this simple starting language (all checked by a computer too). At the end I will discuss some of the exciting recent developments in Homotopy Type Theory. This talk is part of the Trinity Mathematical Society series. ## This talk is included in these lists:Note that ex-directory lists are not shown. |
## Other listsThe Globalization of Music: Origins, Development, & Consequences, c1500–1815 Meeting the Challenge of Healthy Ageing in the 21st Century HEP phenomenology joint Cavendish-DAMTP seminar## Other talksAdaptation in log-concave density estimation Determining structures in situ using cryo-electron tomography:enveloped viruses and coated vesicles Developing and Selecting Tribological Coatings Making Refuge: Academics at Risk CPGJ Reading Group "Space, Borders, Power" Cycles of Revolution in Ukraine |