Graded Modal Types for Memory and Communication Safety - Kent Academic Repository

) " />

) " />

Skip to main content

Kent Academic Repository

Login<br>Admin<br>Dashboards<br>Help

Simple search | Advanced search

Graded Modal Types for Memory and Communication Safety

Marshall, Danielle

(2026)

Graded Modal Types for Memory and Communication Safety.

Doctor of Philosophy (PhD) thesis, University of Kent,.

(KAR id:113723)

PDF

Language: English

This work is licensed under a Creative Commons Attribution 4.0 International License.

Download this file<br>(PDF/3MB)

-->

Preview

Abstract

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.

Item Type:

Thesis

(Doctor of Philosophy (PhD))

Thesis advisor:<br>Orchard, Dominic

Uncontrolled keywords:

graded modal types, linearity, uniqueness, ownership, borrowing, session types

Former Institutional Unit:

There are no former institutional units.

Funders:

Engineering and Physical Sciences Research Council (https://ror.org/0439y7842)

SWORD Depositor:

System Moodle

Depositing User:

System Moodle

Date Deposited:

13 Apr 2026 09:00<br>UTC

Last Modified:

29 Apr 2026 10:38<br>UTC

Resource URI:<br>https://kar.kent.ac.uk/id/eprint/113723 (The current URI for this page, for reference purposes)

University of Kent Author Information

Marshall, Danielle.

Creator's ORCID:

CReDIT Contributor Roles:

Link to SensusAccess

Export to:

RefWorks

EPrints3 XML

BibTeX

CSV

-->

Depositors only (login required):

Total Views<br>Total Views<br>Total Views

Total unique views of this page since July 2020. For more details click on the image.

Feedback