12 citations · 49 across the 13 of their papers we have counts for
14 papers
Communicating Actor Automata -- Modelling Erlang Processes as Communicating Machines
Dominic Orchard, Mihail Munteanu, Paulo Torrens
Brand and Zafiropulo's notion of Communicating Finite-State Machines (CFSMs) provides a succinct and powerful model of message-passing concurrency, based around channels. However,…
Replicate, Reuse, Repeat: Capturing Non-Linear Communication via Session Types and Graded Modal Types
Danielle Marshall, Dominic Orchard
Session types provide guarantees about concurrent behaviour and can be understood through their correspondence with linear logic, with propositions as sessions and proofs as proces…
A Theory of Composing Protocols
Laura Bocchi, Dominic Orchard, A. Laura Voinea
In programming, protocols are everywhere. Protocols describe the pattern of interaction (or communication) between software systems, for example, between a user-space program and t…
Deriving Distributive Laws for Graded Linear Types
Jack Hughes, Michael Vollmer, Dominic Orchard
The recent notion of graded modal types provides a framework for extending type theories with fine-grained data-flow reasoning. The Granule language explores this idea in the conte…
Guiding user annotations for units-of-measure verification
Dominic Orchard, Mistral Contrastin, Matthew Danish +1
This extended abstract reports on previous work of the CamFort project in which we developed an external units-of-measure type system for Fortran code, targeted at scientists. Our…
Graded Modal Dependent Type Theory
Benjamin Moon, Harley Eades, Dominic Orchard
Graded type theories are an emerging paradigm for augmenting the reasoning power of types with parameterizable, fine-grained analyses of program properties. There have been many su…
Graded Hoare Logic and its Categorical Semantics
Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard +1
Deductive verification techniques based on program logics (i.e., the family of Floyd-Hoare logics) are a powerful approach for program reasoning. Recently, there has been a trend o…
Grading Adjoint Logic
Harley Eades, Dominic Orchard
We introduce a new logic that combines Adjoint Logic with Graded Necessity Modalities. This results in a very expressive system capable of controlling when and how structural rules…
Unifying graded and parameterised monads
Dominic Orchard, Philip Wadler, Harley Eades
Monads are a useful tool for structuring effectful features of computation such as state, non-determinism, and continuations. In the last decade, several generalisations of monads…
Proceedings Programming Language Approaches to Concurrency- and Communication-cEntric Software
Francisco Martins, Dominic Orchard
Modern hardware platforms, from the very small to the very large, increasingly provide parallel and distributed computing resources for applications to maximise performance. Many a…
Composing bidirectional programs monadically (with appendices)
Li-yao Xia, Dominic Orchard, Meng Wang
Software frequently converts data from one representation to another and vice versa. Naively specifying both conversion directions separately is error prone and introduces conceptu…
Using session types as an effect system
Dominic Orchard, Nobuko Yoshida
Side effects are a core part of practical programming. However, they are often hard to reason about, particularly in a concurrent setting. We propose a foundation for reasoning abo…
The semantic marriage of monads and effects
Dominic Orchard, Tomas Petricek, Alan Mycroft
Wadler and Thiemann unified type-and-effect systems with monadic semantics via a syntactic correspondence and soundness results with respect to an operational semantics. They conje…
Efficient and Correct Stencil Computation via Pattern Matching and Static Typing
Dominic Orchard, Alan Mycroft
Stencil computations, involving operations over the elements of an array, are a common programming pattern in scientific computing, games, and image processing. As a programming pa…