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.

• Senior Lecturer in the Programming Languages and Systems group
  School of Computing, University of Kent
• Co-director of the Institute of Computing for Climate Science
  Department of Computer Science and Technology, University of Cambridge
• Bye-Fellow at Queens' College, Cambridge

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:

• Institute of Computing for Climate Science
• Granule - Capturing program properties via graded (modal) types
• Programming Languages and Systems for Science Laboratory
• - Verification and static analysis for computational science

PhD Students	Postdocs / RAs
Jack Hughes Vilem Liepelt Daniel Marshall Paulo Torrens Jay Torry Tori Vollmer	Roly Perera

Recent Publications

• 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

• Co-chair: PROPL 2024, TyDe 2021, PADL 2021, PLACES 2019, PLACES 2016, PLE 2015, PLE 2014
• Programme Committee: ICFP 2024, ESOP 2024, APLAS 2023 SRC & Posters, TASE 2023, POPL 2023, Haskell 2022, POPL 2019, BEAT 2019, TyDe 2018, Haskell 2015, Salon des Refusés 2017, IFL 2013
• External Review Commitee: ICFP 2020
• Artefact Evaluation Commitee: ECOOP 2014
• Other: Local organizer of Climate Informatics 2023, Panelist at PLMW 2019

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)