University of Birmingham > Talks@bham > Lab Lunch > Syntax and Semantics of Linear Dependent Types

Syntax and Semantics of Linear Dependent Types

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

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.

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.