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.

This tutorial will include a chance to try exercises and discuss solutions. We therefore recommend installing Granule before the tutorial.
You can download the sources (and binaries for some platforms) for the latest version of Granule here:
https://github.com/granule-project/granule/releases/
Please check also the installation instructions (Granule requires Z3 to be installed).
https://github.com/granule-project/granule/wiki/Installing-Granule
Please let us know if you have any trouble getting set up.