Syntax and Semantics of Linear Dependent Types

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

• Matthijs Vakar (University of Oxford)
• Friday 25 July 2014, 14:00-15:00
• CS 217.

If you have a question about this talk, please contact Neel Krishnaswami.

A type theory is presented that combines (intuitionistic) linear types with type dependency. More precisely, it is a type theory in which linear types are allowed to depend on terms of intuitionistic types. A syntax and (complete) categorical semantics are discussed, the latter in terms of (strict) indexed symmetric monoidal categories with a notion of comprehension. Finally, a few concrete models are touched on.

This talk is part of the Lab Lunch series.

This talk is included in these lists:

• CS 217
• Lab Lunch

Note that ex-directory lists are not shown.