BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Dependent Linear Type Theory via Bunched(less) Implications - Ines
  Wright (University of Cambridge)
DTSTART:20250602T150000Z
DTEND:20250602T160000Z
UID:TALK232951@talks.cam.ac.uk
CONTACT:Dr Meven Lennon-Bertrand
DESCRIPTION: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 thi
 s talk I will discuss work I have been doing for my Master's thesis\, supe
 rvised 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 d
 ependency and identity types of terms which include resources.
LOCATION:FW26\, Computer Laboratory
END:VEVENT
END:VCALENDAR