Resource-oriented programming with graded modal types

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

• Vilem Liepelt, University of Kent
• Thursday 18 April 2019, 14:00-15:00
• FW26.

If you have a question about this talk, please contact Victor Gomes.

Linear types, derived from Girard’s Linear Logic, provide a means to expose safe interfaces to stateful protocols and language features, e.g. channels and file handles. Data is delineated into two camps: unconstrained values which can be consumed or discarded arbitrarily and ‘resources’ which must be used exactly once. Bounded Linear Logic (BLL) [1], allows tracking a more nuanced notion of nonlinearity via the natural numbers semiring which is baked into its proof rules. Our system of Graded Modal Types generalises BLL by parameterising over the resource algebra, thus allowing a wide array of analyses to be captured in the type system.

In this talk we will explore how graded modal types and linearity conveniently extend our typical toolkit of parametric polymorphism and indexed types, allowing us to reason about pure and effectful programs in a novel, resource-oriented, manner. Session typed channels and mutable arrays are just two examples of programming idioms that can be provided in such a language without having to give up safety and compositionality. We will see this in action via Granule [2], our implementation of a functional language with a type system which supports all these features.

1. Girard, Scedrov, Scott (1992)

2. https://github.com/granule-project/granule

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.