Dr Dominic Orchard

My research is at the intersection of types, semantics, and logic, with a focus on programming languages and verification. I also work closely with domain experts in climate science.
I am also a Fellow of the Software Sustainability Institute.

Projects / groups

Key funded projects that I am currently working on, and groups I am leading:

PhD Students

Postdocs / RAs

Recent Publications

  • Functional Ownership through Fractional Uniqueness
    Danielle Marshall, Dominic Orchard
    OOPSLA 2024 [PDF] (BibTeX)
  • On the Operational Theory of the CPS-Calculus: Towards a Theoretical Foundation for IRs
    Paulo Torrens, Dominic Orchard, Cristiano Vasconcellos
    ICFP 2024 [PDF] (BibTeX)
  • Program Synthesis from Graded Types
    Jack Hughes, Dominic Orchard
    ESOP 2024 [PDF] (BibTeX)
  • Communicating Actor Automata – Modelling Erlang Processes as Communicating Machines
    Dominic Orchard, Mihail Munteanu, Paulo Torrens
    PLACES 2023 [PDF] (BibTeX)
  • A Theory of Composing Protocols
    Laura Bocchi, Dominic Orchard, Laura Voinea
    The Art, Science, and Engineering of Programming, 2023 [PDF] (BibTeX)
  • How To Take the Inverse of a Type
    Daniel Marshall, Dominic Orchard
    ECOOP 2022 - Distinguished Paper Award and Distinguished Artifact Award - [PDF]
  • Linearity and Uniqueness: An Entente Cordiale
    Daniel Marshall, Michael Vollmer, Dominic Orchard
    ESOP 2022 [PDF] (BibTeX)
  • Replicate, Reuse, Repeat: Capturing Non-Linear Communication via Session Types and Graded Modal Types
    Daniel Marshall, Dominic Orchard
    PLACES 2022 [PDF] (BibTeX)
  • Linear Exponentials as Graded Modal Types
    Jack Hughes, Daniel Marshall, James Wood, Dominic Orchard
    TLLA 2021 [PDF] (BibTeX)
  • Graded Modal Dependent Type Theory
    Ben Moon, Harley Eades III, Dominic Orchard
    ESOP 2021 [PDF] (BibTeX)
  • Graded Hoare Logic and its Categorical Semantics
    Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard, Tetsuya Sato
    ESOP 2021 [PDF] (BibTeX)
  • Deriving distributive laws for graded linear types
    Jack Hughes, Michael Vollmer, Dominic Orchard
    Post proceedings of Linearity-TLLA 2020 [PDF]
  • Resourceful Program Synthesis from Graded Linear Types
    Jack Hughes, Dominic Orchard
    LOPSTR 2020 - Best paper award - [PDF] (BibTeX)
  • Data-Flow Analyses as Effects and Graded Monads
    Andrej Ivaskovic, Alan Mycroft, Dominic Orchard
    FSCD 2020 [PDF] (BibTeX)
  • Unifying graded and parameterised monads
    Dominic Orchard, Philip Wadler, Harley Eades III
    MSFP 2020 [PDF] (BibTeX)
  • Quantitative Program Reasoning with Graded Modal Types
    Dominic Orchard, Vilem-Benjamin Liepelt, Harley Eades III
    ICFP 2019 [PDF] (BibTeX)
  • Composing Bidirectional Programs Monadically
    Li-yao Xia, Dominic Orchard, Meng Wang
    ESOP 2019 [PDF] [Appendix] (BibTeX)
  • Automatic Reordering for Dataflow Safety of Datalog
    Mistral Contrastin, Dominic Orchard, Andrew Rice
    PPDP 2018 [PDF] (BibTeX)
  • Complexity bounds for container functors and comonads
    Dominic Orchard
    Information and Computation (261) 2018 [PDF] [Publisher PDF] (BibTeX)
  • Verifying spatial properties of array computations
    Dominic Orchard, Mistral Contrastin, Matthew Danish, Andrew Rice
    OOPSLA 2017 [PDF] (BibTeX)
  • Session Types with Linearity in Haskell
    Dominic Orchard, Nobuko Yoshida
    Book chapter in Behavioural Types: from Theory to Tools [PDF] (BibTeX)
  • Units-of-Measure correctness in Fortran programs
    Mistral Contrastin, Andrew Rice, Matthew Danish, Dominic Orchard
    Computing in Science & Engineering, 2016 [PDF] (BibTeX)
  • Combining effects and coeffects via grading
    Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard, Flavien Breuvart, Tarmo Uustalu
    ICFP 2016 [PDF] (BibTeX)
  • Effect Systems Revisited - Control-Flow Algebra and Semantics
    Alan Mycroft, Dominic Orchard, Tomas Petricek
    Semantics, Logics, and Calculi (Festschrift for Hanne Riis Nielson and Flemming Nielson) LNCS, 2016 [PDF] (BibTeX)
  • Effects as sessions, sessions as effects
    Dominic Orchard, Nobuko Yoshida
    POPL 2016 [PDF] (BibTeX)
  • Evolving Fortran types with inferred units-of-measure.
    Dominic Orchard, Andrew Rice, Oleg Oshmyan
    Journal of Computational Science - Special issue on selected papers from ICCS 2015 [PDF] (BibTeX)
  • Using session types as an effect system
    Dominic Orchard, Nobuko Yoshida
    PLACES 2015 [PDF] (BibTeX)
  • Coeffects: a calculus of context-dependent computation
    Tomas Petricek, Dominic Orchard, Alan Mycroft
    ICFP 2014 [PDF] (BibTeX)
  • Temporal semantics for a live coding language
    Samuel Aaron, Dominic Orchard, Alan Blackwell
    FARM 2014 [PDF] (BibTeX)
  • Embedding effect systems in Haskell
    Dominic Orchard, Tomas Petricek
    Haskell 2014 [PDF] (BibTeX)
  • Programming language evolution workshop report
    Raoul-Gabriel Urma, Dominic Orchard, Alan Mycroft
    PLE@ECOOP 2014 [PDF] (BibTeX)
  • A Computational Science Agenda for Programming Language Research
    Dominic Orchard, Andrew Rice
    ICCS 2014 [PDF] (BibTeX)
  • Automatic SIMD vectorization for Haskell
    Leaf Petersen, Dominic Orchard, Neal Glew
    ICFP 2013 [PDF] (BibTeX)
  • Coeffects: Unified Static Analysis of Context-Dependence.
    Tomas Petricek, Dominic Orchard, Alan Mycroft
    ICALP 2013 [PDF] (BibTeX)
  • A Notation for Comonads
    Dominic Orchard, Alan Mycroft
    IFL 2012 [PDF] (BibTeX)
  • The four Rs of programming language design.
    Dominic Orchard
    Onward! Essays 2011 [PDF] (BibTeX)
  • Efficient and Correct Stencil Computation via Pattern Matching and Static Typing
    Dominic Orchard, Alan Mycroft
    DSL 2011 [PDF] (BibTeX)
  • Haskell Type Constraints Unleashed
    Dominic Orchard, Tom Schrijvers
    FLOPS 2010 [PDF] (BibTeX)
  • Ypnos: declarative, parallel structured grid programming
    Dominic Orchard, Max Bolingbroke, Alan Mycroft
    DAMP 2010 [PDF] (BibTeX)
  • muCell - Interdisciplinary Research in Modelling and Simulation of Cell Spatial Behaviour
    Dominic Orchard, Jonathan Gover, Lee Lewis Herrington,, James Lohr, Duncan Stead, Cathy Young, Sara Kalvala
    Reinvention journal 2009 [PDF] (BibTeX)
  • Integrating Lucid's Declarative Dataflow Paradigm into Object-Orientation
    Dominic Orchard, Steve Matthews
    Mathematics in Computer Science 2008 [PDF] (BibTeX)

Service

Previous students and group members

  • Michael Vollmer (post doc 2020-21 went on to be a Lecturer at the University of Kent)
  • Marco Paviotti (post doc 2022 went on to be a Lecturer at the University of Kent
  • Ben Orchard (Research Assistant)
Dominic Orchard's photo

University of Kent logo

University of Cambridge logo