## 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:Note that ex-directory lists are not shown. |
## Other listsSERENE Seminars Featured talks Analysis Reading Seminar 2019/2020## Other talks[Seminar]: Two easy three-body problems [Friday seminar]: Irradiated brown dwarfs in the desert Seminar Signatures of structural criticality and universality in the cellular anatomy of the brain The percolating cluster is invisible to image recognition with deep learning Towards Efficient and Robust Data-Driven Optimization |