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:Note that ex-directory lists are not shown. |
## Other listsTheoretical computer science seminar IMA West Midlands Branch Seminars on Advanced Materials## Other talksLyapunov Design of Two Success-Based Step-Size Adaptation Rules RSLC PhD/Postdoc Seminars (Chemistry) Black-hole driven explosions and the dynamical Universe Causal Sets, Discrete Gravity PTC Seminar Two problems in extremal graph theory |