- Graded Modal Dependent Type Theory theorypractice
- Ben Moon, Harley Eades III, Dominic Orchard
- ESOP 2021
- Accompanying release of Gerty v0.1.0
- Graded Hoare Logic and its Categorical Semantics theory
- Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard, Tetsuya Sato
- ESOP 2021
- A graded dependent type system with a usage-aware semantics theory
- Pritam Choudhury, Harley Eades III, Richard Eisenberg, Stephanie Weirich
- POPL 2021
- Resourceful program synthesis from graded linear types practice theory
Towards Graded Modal Dependent Types (extended abstract) theory
- Benjamin Moon, Harley Eades III, and Dominic Orchard
- 2-page extended abstract at TyDe 2020 introducing ideas on Graded Modal Dependent Type Theory.
- Deriving distributive laws for graded linear types practice theory draft
Grading Adjoint Logic theory
- Harley Eades III, Dominic Orchard
- 2-page extended abstract at LINEARITY/TLLA 2020.
- Andrej Ivašković, Alan Mycroft, Dominic Orchard
- FSCD 2020 (LIPIcs, Volume 167)
- Additional material (proofs and code)
- Dominic Orchard, Philip Wadler, Harley Eades III
- MSFP 2020
- A category theoretic study of the relationship between graded and parameterised monads, via the notion of a category-graded monad.
Quantitative program reasoning with graded modal types theorypractice
- Dominic Orchard, Vilem-Benjamin Liepelt, Harley Eades III
- In the Proceedings of the ACM on Programming Languages, Volume 3(ICFP), 2019.
- The Granule paper: describes much of our approach and the state of the language, detailing the type system with various example.
- Version with appendices
- Associated code release
Gram: A linear functional language with graded modal types (extended abstract) practice
- Dominic Orchard and Vilem-Benjamin Liepelt
- 2-page extended abstract at TLLA 2017 with early ideas about the language, before the name was changed to Granule.
- Marco Gaboardi, Shinya Katsumata, Dominic Orchard, Flavien Breuvart, Tarmo Uustalu
- ICFP 2016
- The system in this paper pre-dates Granule, but it provides some core ideas which are at the core of Granule, although Granule adds a lot more language features on top.