Publications

• A Mixed Linear and Graded Logic: Proofs, Terms, and Modelstheory
  • Victoria Vollmer, Danielle Marshall, Harley Eades III, Dominic Orchard
  • CSL 2025
• Non-linear communication via graded modal session types theorypractice
  • Danielle Marshall, Dominic Orchard
  • Information & Computation
• Program Synthesis from Graded Types practice/synthesis
  • Jack Hughes, Dominic Orchard
  • Additional appendix
  • ESOP 2024
• Functional Ownership through Fractional Uniqueness theorypractice
  • Danielle Marshall, Dominic Orchard
  • Additional appendices
  • Artefact deposit
  • OOPSLA 2024
• Combining Dependency, Grades, and Adjoint Logic theory
  • Peter Hanukaev, Harley Eades
  • TyDe 2023
• How to Take the Inverse of a Type theory
  • Danielle Marshall, Dominic Orchard
  • ECOOP 2022 (functional pearl)
• Linearity and Uniqueness: An Entente Cordiale theorypractice
  • Danielle Marshall, Michael Vollmer, Dominic Orchard
  • ESOP 2022
  • Supplementary material: appendices
• Replicate, Reuse, Repeat: Capturing Non-Linear Communication via Session Types and Graded Modal Types practice
  • Danielle Marshall, Dominic Orchard
  • PLACES 2022
• Linear Exponentials as Graded Modal Types theory
  • Jack Hughes, Danielle Marshall, James Wood, Dominic Orchard
  • 8-page extended abstract at TLLA 2021.
• 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 theoryaward
  • Jack Hughes, Dominic Orchard
  • Version accepted for post-proceedings at LOPSTR 2020.
  • Granule implementation available here.
  • Won Best Paper Award.
• 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
  • Jack Hughes, Michael Vollmer, Dominic Orchard
  • Proceedings of TLLA 2020
  • (See also this earlier 2-page extended abstract accepted at LINEARITY/TLLA 2020).
• Grading Adjoint Logic theory
  • Harley Eades III, Dominic Orchard
  • 2-page extended abstract at LINEARITY/TLLA 2020.
• Data-flow analyses as effects and graded monads theory
  • Andrej Ivašković, Alan Mycroft, Dominic Orchard
  • FSCD 2020 (LIPIcs, Volume 167)
  • Additional material (proofs and code)
• Unifying graded and parameterised monads theory
  • 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.
• Combining effects and coeffects via grading theory
  • 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.