## Syntax and Semantics of Linear Dependent TypesAdd 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
- Computer Science Departmental Series
- Computer Science Distinguished Seminars
- Lab Lunch
- Theoretical computer science seminar
Note that ex-directory lists are not shown. |
## Other listsFeatured lists 'Roles' Postgraduate Gender and Sexuality Network Discussion Filling in the blank – I will be ….... in 2050’## Other talks |