Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Mon 14 Jan 2019 09:00 - 10:30 at Sala VI - Tutorial 3A
Mon 14 Jan 2019 11:00 - 12:30 at Sala VI - Tutorial 3B

Linear types have long been heralded as a mechanism for enforcing strict adherence to resource-based protocols, e.g., file handles, operation system APIs, and communication protocols in concurrency. Recent work has seen linear types become an increasingly popular topic in our community, with the rise in the work on session types, with new proposed extensions to Haskell for linear types, and with languages such as Rust and ATS. This tutorial provides an introduction to linear types and a look at the state-of-the-art in type systems extending linear types with graded modal types as a basis for more fine-grained program reasoning as embodied by the Granule programming language. Granule combines linear types with lightweight dependent types and graded modal types, providing a rich type system for enforcing fine-grained resource constraints on top of a functional language in the style of Haskell/ML. This tutorial will cover both the theoretical and practical aspects of linear and graded modal types, with an opportunity to try Granule via exercises as well an introduction to the research context and recent work in the literature.

Mon 14 Jan

Displayed time zone: Belfast change

09:00 - 10:30
Tutorial 3ATutorialFest at Sala VI
09:00
90m
Talk
[T3] Linear and Graded Modal Types for Fine-Grained Program Reasoning
TutorialFest
Dominic Orchard University of Kent, UK, Harley D. Eades III Augusta University, Vilem-Benjamin Liepelt University of Kent, UK
11:00 - 12:30
Tutorial 3BTutorialFest at Sala VI
11:00
90m
Talk
[T3] Linear and Graded Modal Types for Fine-Grained Program Reasoning
TutorialFest
Dominic Orchard University of Kent, UK, Harley D. Eades III Augusta University, Vilem-Benjamin Liepelt University of Kent, UK