research.md

layout	title
page	Publications

Publications

• 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.