14 citations · 36 across the 11 of their papers we have counts for
11 papers
Denotational reasoning for asynchronous multiparty session types
Dylan McDermott, Nobuko Yoshida
We provide the first denotational semantics for asynchronous multiparty session types with precise asynchronous subtyping. Our semantics enables us to reason about asynchronous mes…
Presheaves and cocompletions in formal category theory
Nathanael Arkor, Dylan McDermott
We study the relationship between presheaf constructions and free cocompletions in the context of formal category theory, elucidating the coincidence between the two concepts in fa…
The nerve theorem for relative monads
Nathanael Arkor, Dylan McDermott
A fundamental result in the theory of monads is the characterisation of the category of algebras for a monad in terms of a pullback of the category of presheaves on the category of…
Canonical Gradings of Monads
Flavien Breuvart, Dylan McDermott, Tarmo Uustalu
We define a notion of grading of a monoid T in a monoidal category C, relative to a class of morphisms M (which provide a notion of M-subobject). We show that, under reasonable con…
Relative monadicity
Nathanael Arkor, Dylan McDermott
We establish a relative monadicity theorem for relative monads with dense roots in a virtual equipment, specialising to a relative monadicity theorem for enriched relative monads.…
The formal theory of relative monads
Nathanael Arkor, Dylan McDermott
We develop the theory of relative monads and relative adjunctions in a virtual equipment, extending the theory of monads and adjunctions in a 2-category. The theory of relative com…
What Makes a Strong Monad?
Dylan McDermott, Tarmo Uustalu
Strong monads are important for several applications, in particular, in the denotational semantics of effectful languages, where strength is needed to sequence computations that ha…
Galois connecting call-by-value and call-by-name
Dylan McDermott, Alan Mycroft
We establish a general framework for reasoning about the relationship between call-by-value and call-by-name. In languages with computational effects, call-by-value and call-by-nam…
Abstract clones for abstract syntax
Nathanael Arkor, Dylan McDermott
We give a formal treatment of simple type theories, such as the simply-typed -calculus, using the framework of abstract clones. Abstract clones traditionally describe first-orde…
Factorisation systems for logical relations and monadic lifting in type-and-effect system semantics
Ohad Kammar, Dylan McDermott
Type-and-effect systems incorporate information about the computational effects, e.g., state mutation, probabilistic choice, or I/O, a program phrase may invoke alongside its retur…
A monadic solution to the Cartwright-Felleisen-Wadler conjecture
Ohad Kammar, Dylan McDermott
Given a programming language, can we give a monadic denotational semantics that is stable under language extension? Models containing only a single monad are not stable. Models bas…