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

  Browse A-Z

Log in

System Admin (disabled)details Birmingham usersdetails No account?details

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

A continuous computational interpretation of type theories

Add to your list(s) Download to your calendar using vCal

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Bravo Cold Atoms Molecular and Medical Physics Seminar Series

Other talks

Generalised hydrodynamics and universalities of transport in integrable (and non-integrable) spin chains TBA TBA Best Response Dynamics on Random Graphs TBA TBA
 

Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on talks.cam from the University of Cambridge.