![]() |
![]() |
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
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 listsCargo School of Chemistry Seminars Applied Mathematics Seminar SeriesOther talksWell Founded Coalgebras Modelling uncertainty in image analysis. Seminar: TBA Seminar: TBA Spectrally selective metasurfaces based on bound states in the continuum: a versatile platform for enhanced light-matter coupling Seminar: TBA |