Name: Valeria de Paiva, "Going Without: a modality and its role"
Start: 2019-03-01T19:00:00-08:00
End: 2019-03-01T21:00:00-08:00
Location: 220, Alumni Science Hall, Santa Clara University

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.

Vlad Patryshev

Bay Area Categories And Types

Technology

Logic

Category Theory

Functional Programming

Type Theory

Functors and Monads

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

220, Alumni Science Hall, Santa Clara University

Share

Bay Area Categories And Types

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

Bay Area Categories And Types

Details

Members are also interested in