A continuous computational interpretation of type theories

Add 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
• Lab Lunch

Note that ex-directory lists are not shown.