University of Birmingham > Talks@bham > Lab Lunch > A continuous computational interpretation of type theories

## A continuous computational interpretation of type theoriesAdd to your list(s) Download to your calendar using vCal - Chuangjie Xu (University of Birmingham)
- Monday 09 March 2015, 12:00-13:00
- CS 217.
If you have a question about this talk, please contact Uday Reddy. We develop a constructive variation of Johnstone’s topological topos to provide a computational interpretation of type theory validating Brouwer’s uniform-continuity principle, so that type-theoretic proofs with the principle as an assumption have computational content. The construction of our model and the verification of the uniform-continuity principle have been formalized in intensional Martin-Löf type theory in Agda notation. Hence we obtain a program of computing least moduli of uniform continuity! This talk is part of the Lab Lunch series. ## This talk is included in these lists:- CS 217
- Computer Science Departmental Series
- Computer Science Distinguished Seminars
- Lab Lunch
- Theoretical computer science seminar
- computer sience
Note that ex-directory lists are not shown. |
## Other listsBiosciences seminars Computer Science Distinguished Seminars Theoretical Physics Seminars## Other talksAdvancing biomedical photoacoustic imaging using structured light and optical microresonators TBC |