Graded Modal Types for Memory and Communication Safety

Using types to delineate various kinds of values is a ubiquitous technique in modern programming. However, one common pattern is for a piece of data to represent access to a resource (such as a reference or channel) which needs to be used in a certain way. This presents challenges for using types to ensure software correctness, as we need to reason about how data is used rather than what data is being used.

Linear types are one approach to this problem, separating data that can be used any number of times from data that will be used exactly once. Graded type systems such as the one underlying the Granule research language generalise this to allow for more precise restrictions on exactly how data must be used. However, existing graded systems generally focus on describing local properties pertaining to single pieces of data, whereas sometimes we are interested in global properties that hold over an entire program.

In this thesis, we demonstrate that the framework of graded types can be extended to allow for the verification of global program behaviour, encapsulating key properties from the paradigms of both memory and communication safety.

First, we discuss memory safety. We describe in detail the relationship between the two similar but contrasting ideas of linear types and uniqueness types, which ensure that only a single mutable reference to a value can exist, and then embed uniqueness into an existing graded calculus by introducing a new flavour of modality. We then extend this system to describe more general notions of ownership and borrowing as popularised by the Rust programming language, using a new form of fractional grading which allows for multiple immutable references to a single value. The overall system is made formal through a heap-based operational model.

Second, we discuss communication safety. We first present a formalisation of session types alongside grading, using an operational model extended with processes and channels to show that concurrency issues are ruled out and resolving problems with Granule's prior instantiation of session-typed channels. We then introduce additional primitives for non-linear communication, allowing for essential communication patterns that cannot be described with purely linear session types to be precisely represented. All of the systems we discuss are fully implemented in Granule.