Valeria de Paiva, "Going Without: a modality and its role"

Linear type theories have been with us for more than 25 years, from the beginning of Linear Logic, and they still have much to teach us. I want to discuss and compare three linear type theories and show how an overlooked system has much potential to help with open issues in modal type theory. We discuss the Linear Lambda Calculus (Benton et al), DILL (the Dual Intuitionistic Linear Logic) and the Linear-non-Linear (LNL) Type Theories. Then we recall how DILL can be transformed into ILT (Maietti et al 200), a type theory without a modality, but with two functions spaces, and what we gain with this transformation. Finally, we speculate on how this transformation might be be helpful for modal type theory and its models.