University of Birmingham > Talks@bham > Theoretical computer science seminar > Effectfully gardening with the Pythia

## Effectfully gardening with the PythiaAdd to your list(s) Download to your calendar using vCal - Martin Baillon (INRIA)
- Friday 03 March 2023, 11:00-11:50
- LG23, Computer Science // Zoom.
If you have a question about this talk, please contact George Kaye. Note unusual time because of interviews We generalize to a rich dependent type theory a proof originally developed by Escardó that all System T functionals are continuous. It relies on the definition of a syntactic model of Baclofen Type Theory, a type theory where dependent elimination must be strict, into the Calculus of Inductive Constructions. The model is given by three translations: the axiom translation, that adds an oracle to the context; the branching translation, based on the dialogue monad, turning every type into a tree; and finally, a layer of algebraic binary parametricity, binding together the two translations. In the resulting type theory, every function f : (N → N) → N is externally continuous. This talk is part of the Theoretical computer science seminar series. ## This talk is included in these lists:- Computer Science Departmental Series
- Computer Science Distinguished Seminars
- LG23, Computer Science // Zoom
- Theoretical computer science seminar
- computer sience
Note that ex-directory lists are not shown. |
## Other listsEPS - College Research and KT Support Activities Computer Security Seminars Postgraduate Algebra Seminar## Other talksLife : it’s out there, but what and why ? TBC TBA TBA TBA The tragic destiny of Mileva Marić Einstein |