University of Birmingham > Talks@bham > Theoretical computer science seminar > Worldly Type Systems

Worldly Type Systems

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


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