Dependent Linear Type Theory via Bunched(less) Implications

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

• Ines Wright (University of Cambridge)
• Monday 02 June 2025, 16:00-17:00
• FW26, Computer Laboratory.

If you have a question about this talk, please contact Dr Meven Lennon-Bertrand.

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.

This talk is part of the SANDWICH Seminar (Computer Laboratory) series.

This talk is included in these lists:

• FW26, Computer Laboratory
• tcw57’s list

Note that ex-directory lists are not shown.