BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Resource-oriented programming with graded modal types - Vilem Liep
 elt\, University of Kent
DTSTART:20190418T130000Z
DTEND:20190418T140000Z
UID:TALK121921@talks.cam.ac.uk
CONTACT:Victor Gomes
DESCRIPTION:Linear types\, derived from Girard's Linear Logic\, provide a 
 means to expose safe\ninterfaces to stateful protocols and language featur
 es\, e.g. channels and file\nhandles. Data is delineated into two camps: u
 nconstrained values which can be\nconsumed or discarded arbitrarily and 'r
 esources' which must be used exactly\nonce. Bounded Linear Logic (BLL) [1]
 \, allows tracking a more nuanced notion of\nnonlinearity via the natural 
 numbers semiring which is baked into its proof\nrules. Our system of Grade
 d Modal Types generalises BLL by parameterising over\nthe resource algebra
 \, thus allowing a wide array of analyses to be captured in\nthe type syst
 em.\n\nIn this talk we will explore how graded modal types and linearity c
 onveniently\nextend our typical toolkit of parametric polymorphism and ind
 exed types\,\nallowing us to reason about pure and effectful programs in a
  novel\,\nresource-oriented\, manner. Session typed channels and mutable a
 rrays are just\ntwo examples of programming idioms that can be provided in
  such a language\nwithout having to give up safety and compositionality. W
 e will see this in\naction via Granule [2]\, our implementation of a funct
 ional language with a type\nsystem which supports all these features.\n\n1
 . Girard\, Scedrov\, Scott (1992)\n\n2. https://github.com/granule-project
 /granule
LOCATION:FW26
END:VEVENT
END:VCALENDAR