The Granule Project
The Granule project is an ambitious research project whose focus is to capture more and more intensional properties of programs at the type-level, that is, how a program computes not just what it computes. Our primary mechanism for doing this is via the relatively new notion of graded types in concert with other typing mechanisms like linear types and dependent types. For example, graded modal types can be combined with linear types to make resource sensitivity an integral aspect of a programming language, precisely enforcing resource usage throughout the language. Other examples include capturing fine-grained information about side effects, data use, privacy levels, cost, and permissions via various kinds of (co)effect types captures via graded modal types.
Our project spans theoretical and practical work. We are actively developing an implementation of a language with graded, linear, and indexed types called Granule based on our research. In addition, we are developing a new dependent type theory that will greatly expand the expressive power of Granule’s type system. This is currently implemented in another language called Gerty.
News
April 2024 paper
We are excited to announce two new publications from our group:
- Program Synthesis from Graded Types by Jack Hughes and Dominic Orchard to appear at ESOP 2024.
- Functional Ownership through Fractional Uniqueness by Danielle Marshall and Dominic Orchard to appear at OOPSLA 2024.
September 2023 staff
Riccardo Bianchini is visiting us for two weeks in September, and talking about his work on multi-graded Featherweight Java.
August 2023 paper
Harley and Peter have a new paper on Combining Dependency, Grades, and Adjoint Logic published at TyDe 2023 (Type-Driven Development) co-located with ICFP 2023.
July 2023 misc
Dominic presented the work of the Granule project in 6 hours of teaching at the Scottish Programming Languages and Verification summer school.
January 2023 staff
Congratulations to Dr Marco Paviotti on getting a lectureship at Kent! Thankfully Marco will still be working with us in his new role. Well done Marco!
May 2022 staff
We are very pleased to welcome Dr Marco Paviotti to the project at the University of Kent. Marco joins as a Senior Research Associate with expertise in semantics, category theory, recursion schemes, and mathematical logic.
March 2022 paper
Danielle and Dominic have a new paper accepted at PLACES 2022 on capturing various kinds of non-linear communication and concurrent behaviour in a type-based discipline by combining session types and graded types.
- Replicate, Reuse, Repeat: Capturing Non-Linear Communication via Session Types and Graded Modal Types (Danielle Marshall and Dominic Orchard).
February 2022 paper
Danielle and Dominic have a pearl accepted to ECOOP 2022 on how linear functions consuming values can be understood algebraically as a multiplicative inverse to the type of those values, discussing some of the applications using both Haskell and Granule. This paper won a Distinguished Paper Award and a Distinguished Artifact Award.
- How to Take the Inverse of a Type (Danielle Marshall and Dominic Orchard).
January 2022 paper
Danielle, Michael and Dominic have a paper accepted to ESOP 2022 on unifying the closely related notions of linearity and uniqueness in a single type system, and implementing this theory to demonstrate the practical benefits of uniqueness types in Granule.
- Linearity and Uniqueness: An Entente Cordiale (Danielle Marshall, Michael Vollmer, and Dominic Orchard).
January 2022 award
Danielle has been awarded first place in the Student Research Competition at POPL 2022, for her ongoing work on unifying the closely related concepts of linearity, uniqueness and ownership using Granule’s expressive type system.
June 2021 paper
The Granule project has an abstract accepted for presentation at TLLA 2021:
- Linear Exponentials as Graded Modal Types (Jack Hughes, Danielle Marshall, James Wood, and Dominic Orchard).
May 2021 job award
Harley has been awarded a National Science Foundation grant on:
Semantically and Practically Generalizing Graded Modal Types
to recruit a PhD Student and continue his work on exploring the expressive power of the theory of graded modal types. Checkout the blog post here.
March 2021 implementation
We are excited to release Gerty v0.1.0, our implementation of our work on graded modal dependent type theory.
December 2020 paper
-
We made an “end of the year review” video summarising what we have been up to in 2020. Watch on Youtube.
-
Ben, Harley, and Dominic have a new paper on a new graded modal dependent type theory entitled “Graded Modal Dependent Type Theory”. To appear at ESOP 2021. Find the preprint here.
-
November 2020 paper
Harley has a new paper on a new graded dependent type system called \(\GraD{}\) entitled “A graded dependent type system with a usage-aware semantics”, joint work with Pritram Choudhury, Richard A. Eisenberg, and Stephanie Weirich. To appear at POPL 2021. Find the preprint here.
October 2020 paper
We have two new draft papers online (under review):
- Graded Modal Dependent Type Theory (Benjamin Moon, Harley Eades III, Dominic Orchard)
- Deriving distributive laws for graded linear types (Jack Hughes, Michael Vollmer, Dominic Orchard).
September 2020 paper award
Jack and Dominic have a new paper about program synthesis from linear and graded modal types, demonstrated in Granule, accepted to LOPSTR 2020, entitled “Resourceful Program Synthesis from Graded Linear Types”. The version from the pre-proceedings can be found here. This paper won the LOPSTR 2020 Best Paper Award.
June 2020 paper
The Granule project had three abstracts accepted for presentation at LINEARITY/TLLA 2020:
- Jack Hughes and Dominic Orchard. Deriving distributive laws for graded linear types
- Aubrey Bryant and Harley Eades III. The Graded Lambek Calculus
- Harley Eades III and Dominic Orchard. Grading Adjoint Logic
For full access to each abstract see the Publications section.
April 2020 paper
Dominic has a new paper capturing classical data flow analysis via graded monadic semantics accepted to FSCD 2020, entitled “Data-flow analyses as effects and graded monads”, joint with Andrej Ivašković and Alan Mycroft. in the proceedings here.
March 2020 job
The Granule project is hiring a 2-year post-doctoral researcher to work at the University of Kent! Details of how to apply here. Closing date for applications is Friday 8th May 2020.
March 2020 paper
We have a new paper on the relationship between graded monads and parameterised monads accepted to MSFP 2020. Preprint available online, updated to the final version soon.