So, happy new year! See many of you in 2019. I hope you have a great start to the year. I’m looking forward to travelling to Lisbon shortly for POPL 2019 where I will be giving a tutorial on the Granule project joint with Harley Eades and my student Vilem Liepelt. Vilem Liepelt Vilem is a Software Engineer with a strong affinity for functional programming and an interest in static analysis and compilers. He is currently doing a Ph.D. Under Dominic Orchard at the University of Kent, where he is researching the use of linearity and graded modal types for resource aware type systems and compilers.
POPL 2019 (series) /
TutorialFest /
[T3] Linear and Graded Modal Types for Fine-Grained Program Reasoning
Dominic Orchard, Harley D. Eades III, Vilem-Benjamin Liepelt
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
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
09:00 - 10:30: TutorialFest - Tutorial 3A at Sala VI | |||||||||||||||||||||||||||||||||||||||||
09:00 - 10:30 Talk | Dominic OrchardUniversity of Kent, UK, Harley D. Eades IIIAugusta University, Vilem-Benjamin LiepeltUniversity of Kent, UK |
11:00 - 12:30: TutorialFest - Tutorial 3B at Sala VI | |||||||||||||||||||||||||||||||||||||||||
11:00 - 12:30 Talk | Dominic OrchardUniversity of Kent, UK, Harley D. Eades IIIAugusta University, Vilem-Benjamin LiepeltUniversity of Kent, UK |