Publications

• 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
  • Jack Hughes, Dominic Orchard
  • Version accepted for post-proceedings at LOPSTR 2020.
  • Granule implementation available here.

• 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
  • Jack Hughes, Michael Vollmer, Dominic Orchard
  • Submitted to EPTCS as part 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.