## Worldly Type SystemsAdd to your list(s) Download to your calendar using vCal - Conor McBride (University of Strathclyde)
- Friday 06 February 2015, 16:00-17:00
- CS 245.
If you have a question about this talk, please contact Neel Krishnaswami. I refine a dependent type theory with a system of “worlds” that say “where” things are, separately from what they are. Worlds are preordered by “accessibility”, with the variable rule ensuring that information flows only in accordance. The variable rule thus represents a promise which we must keep by establishing that upward transportation of all constructions is admissible. Types thus need to be portable, which provokes some fresh thinking about how we manage quantification. The payoff is that any upward-closed set of worlds admits a Church-to-Curry-style erasure. I’ll discuss a variety of situations which might be modelled by worldly type systems, not least the indexing of algebraic effects. This talk is part of the Theoretical computer science seminar series. ## This talk is included in these lists:- CS 245
- Computer Science Departmental Series
- Computer Science Distinguished Seminars
- Theoretical computer science seminar
- computer sience
Note that ex-directory lists are not shown. |
## Other listsMetamaterials Research Group Seminars Postgraduate Algebra Seminar Virtual Harmonic Analysis Seminar## Other talksTBC Module tensor categories and the Landau-Ginzburg/conformal field theory correspondence Hidden Markov Model in Multiple Testing on Dependent Data Advancing biomedical photoacoustic imaging using structured light and optical microresonators [Colloquium:] Aperture Fever: The Extremely Large Telescope Theory: This is moved to next year, 2023 ! |