Worldly type systems

Conor McBride

Dept. of Computer and Information Sciences
University of Strathclyde

Thursday, 27 February 2014, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101

Abstract: 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. 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.

ERDF
Tarmo Uustalu
Last update 25.2.2014