![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Monday 02 June 2025, 16:00-17:00
Dependent Linear Type Theory via Bunched(less) Implications
- 👤 Speaker: Ines Wright (University of Cambridge)
- 📅 Date & Time: Monday 02 June 2025, 16:00 - 17:00
- 📍 Venue: FW26, Computer Laboratory
Questions? Contact
Dr Meven Lennon-Bertrand
Abstract
Introducing the `number-of-usages` reading of linear variables to dependent type theory has in prior work resulted in type theories with dependencies and identity types restricted to closed linear terms. In this talk I will discuss work I have been doing for my Master’s thesis, supervised by Neel Krishnaswami, applying the ownership reading of resources as seen in the logic of bunched implications to dependent types, with the goal of designing a dependently typed bunched implications which allows dependency and identity types of terms which include resources.
Series This talk is part of the SANDWICH Seminar (Computer Laboratory) series.
Included in Lists
Note: Ex-directory lists are not shown.