I am currently a postdoc in ICETCS at Reykjavik University, working with Tarmo Uustalu on quantified computational effects and interaction.
Previously I was a PhD student in the Programming, Logic and Semantics group of the University of Cambridge Computer Laboratory. I worked with Alan Mycroft on the theory of programming languages with computational effects, including reasoning about evaluation order, and proving correctness of program transformations.
Drafts

Relative monadicity.
Nathanael Arkor and Dylan McDermott.
Last updated: May 2023.
arXivabstract
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. In particular, for a dense Vfunctor j : A → E, a Vfunctor r : D → E is jmonadic if and only if r has a left jrelative adjoint and creates jabsolute colimits. We also establish a pasting law for relative adjunctions, and examine its interaction with relative monadicity. As a consequence, we derive necessary and sufficient conditions for the composite of a Vfunctor with a jmonadic Vfunctor to itself be jmonadic.

The formal theory of relative monads.
Nathanael Arkor and Dylan McDermott.
Last updated: May 2023.
arXivabstract
We develop the theory of relative monads and relative adjunctions in a virtual equipment, extending the theory of monads and adjunctions in a 2category. The theory of relative comonads and relative coadjunctions follows by duality. While some aspects of the theory behave analogously to the nonrelative setting, others require new insights. In particular, the universal properties that define the algebraobject and the opalgebraobject for a monad qua trivial relative monad are stronger than the classical notions of algebraobject and opalgebraobject for a monad qua monad. Inter alia, we prove a number of representation theorems for relative monads, establishing the unity of several concepts in the literature, including the devices of Walters, the jmonads of Diers, and the relative monads of Altenkirch, Chapman, and Uustalu. A motivating setting is the virtual equipment VCat of categories enriched in a monoidal category V, though many of our results are new even for V = Set.

Galois connecting callbyvalue and callbyname. (Extended version.)
Dylan McDermott and Alan Mycroft.
Last updated: December 2023.
PDFabstract
We establish a general framework for reasoning about the relationship between callbyvalue and callbyname.
In languages with computational effects, callbyvalue and callbyname executions of programs often have different, but related, observable behaviours. For example, if a program might diverge but otherwise has no effects, then whenever it terminates under callbyvalue, it terminates with the same result under callbyname. We propose a technique for stating and proving these properties. The key ingredient is Levy's callbypushvalue calculus, which we use as a framework for reasoning about evaluation orders. We show that the callbyvalue and callbyname translations of expressions into callbypushvalue have related observable behaviour under certain conditions on computational effects, which we identify. We then use this fact to construct maps between the callbyvalue and callbyname interpretations of types, and identify further properties of effects that imply these maps form a Galois connection. These properties hold for some computational effects (such as divergence), but not others (such as mutable state). This gives rise to a general reasoning principle that relates callbyvalue and callbyname. We apply the reasoning principle to example computational effects including divergence and nondeterminism.

Higherorder algebraic theories.
Nathanael Arkor and Dylan McDermott.
Last updated: January 2021. See Chapter 4 of Nathanael's thesis for a more recent account.
PDFabstract
Algebraic theories give a presentationfree categorical formulation of universal algebraic structure: objects equipped with firstorder operators, subject to equational laws. Similarly, higherorder algebraic theories describe objects equipped with higherorder, variablebinding operators, such as logical quantifiers or λabstraction. While higherorder structures abound in mathematics and computer science, there exists no systematic treatment in the spirit of that for firstorder structure. This has led to a proliferation of variations of higherorder theory, and consequently a lacklustre general understanding. We take the first steps to rectify this, defining a notion of multisorted higherorder algebraic theory and carrying out a development analogous to that of the firstorder setting. In addition to unifying various previous notions, we (1) establish a correspondence between higherorder algebraic theories and a class of (relative) monads, whose algebras describe the closedterm structure of the corresponding theories; (2) prove that the categories of higherorder algebraic theories, and of the term algebras for a higherorder algebraic theory, are locally strongly finitely presentable; (3) give a new explanation for the apparent asymmetry between models of algebraic theories in the category of sets, and models in arbitrary cartesian categories.
Publications

Galois connecting callbyvalue and callbyname.
Dylan McDermott and Alan Mycroft.
Logical Methods in Computer Science. (To appear.)
draftabstract
We establish a general framework for reasoning about the relationship between callbyvalue and callbyname.
In languages with computational effects, callbyvalue and callbyname executions of programs often have different, but related, observable behaviours. For example, if a program might diverge but otherwise has no effects, then whenever it terminates under callbyvalue, it terminates with the same result under callbyname. We propose a technique for stating and proving these properties. The key ingredient is Levy’s callbypushvalue calculus, which we use as a framework for reasoning about evaluation orders. We show that the callbyvalue and callbyname translations of expressions into callbypushvalue have related observable behaviour under certain conditions on computational effects, which we identify. We then use this fact to construct maps between the callbyvalue and callbyname interpretations of types, and identify further properties of effects that imply these maps form a Galois connection. These properties hold for some computational effects (such as divergence), but not others (such as mutable state). This gives rise to a general reasoning principle that relates callbyvalue and callbyname. We apply the reasoning principle to example computational effects including divergence and nondeterminism.

A type system with subtyping for WebAssembly's stack polymorphism.
Dylan McDermott, Yasuaki Morita, and Tarmo Uustalu.
ICTAC 2022. doi:10.1007/9783031177156_20
local PDFabstract
We propose a new type system for WebAssembly. It is a refinement of the type system from the language specification and is based on type qualifiers and subtyping. In the WebAssembly specification, a typable instruction sequence gets many different types, depending in particular on whether it contains instructions such as br (unconditional branch) that are stackpolymorphic in an unusual way. But one cannot single out a canonical type for a typable instruction sequence satisfactorily. We introduce qualifiers on code types to distinguish between the two flavors of stack polymorphism that occur in WebAssembly and a subtyping relation on such qualified types. Our type system gives every typable instruction sequence a canonical type that is principal. We show that the new type system is in a precise relationship to the type system given in the WebAssembly specification. In addition, we describe a typed functionalstyle bigstep semantics based on this new type system underpinned by an indexed graded monad and prove that it prevents stackmanipulation related runtime errors. We have formalized our type system, inference algorithm, and semantics in Agda.

Flexibly graded monads and graded algebras.
Dylan McDermott and Tarmo Uustalu.
MPC 2022. doi:10.1007/9783031169120_4
local PDF, slidesabstract
When modelling sideeffects using a monad, we need to equip the monad with effectful operations. This can be done by noting that each algebra of the monad carries interpretations of the desired operations. We consider the analogous situation for graded monads, which are a generalization of monads that enable us to track quantitative information about sideeffects. Grading makes a significant difference: while many graded monads of interest can be equipped with similar operations, the algebras often cannot. We explain where these operations come from for graded monads. To do this, we introduce the notion of flexibly graded monad, for which the situation is similar to the situation for ordinary monads. We then show that each flexibly graded monad induces a canonical graded monad in such a way that operations for the flexibly graded monad carry over to the graded monad. In doing this, we reformulate grading in terms of locally graded categories, showing in particular that graded monads are a particular kind of relative monad. We propose that locally graded categories are a useful setting for work on grading in general.

Flexible presentations of graded monads.
Shinya Katsumata, Dylan McDermott, Tarmo Uustalu, and Nicolas Wu.
ICFP 2022. doi:10.1145/3547654
local PDF, slidesabstract
A large class of monads used to model computational effects have natural presentations by operations and equations, for example, the list monad can be presented by a constant and a binary operation subject to unitality and associativity. Graded monads are a generalization of monads that enable us to track quantitative information about the effects being modelled. Correspondingly, a large class of graded monads can be presented using an existing notion of graded presentation. However, the existing notion has some deficiencies, in particular many effects do not have natural graded presentations.
We introduce a notion of flexibly graded presentation that does not suffer from these issues, and develop the associated theory. We show that every flexibly graded presentation induces a graded monad equipped with interpretations of the operations of the presentation, and that all graded monads satisfying a particular condition on colimits have a flexibly graded presentation. As part of this, we show that the usual algebrapreserving correspondence between presentations and a class of monads transfers to an algebrapreserving correspondence between flexibly graded presentations and a class of flexibly graded monads.

Canonical gradings of monads.
Flavien Breuvart, Dylan McDermott, and Tarmo Uustalu.
ACT 2022.10.4204/EPTCS.380.1
local PDF, slidesabstract
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 Msubobject). We show that, under reasonable conditions (including that M forms a factorization system), there is a canonical grading of T. Our application is to graded monads and models of computational effects. We demonstrate our results by characterizing the canonical gradings of a number of monads, for which C is endofunctors with composition. We also show that we can obtain canonical grades for algebraic operations.

What makes a strong monad?
Dylan McDermott and Tarmo Uustalu.
MSFP 2022. doi:10.4204/EPTCS.360.6
local PDF, slidesabstract
Strong monads are important for several applications, in particular, in the denotational semantics of effectful languages, where strength is needed to sequence computations that have free variables. Strength is nontrivial: it can be difficult to determine whether a monad has any strength at all, and monads can be strong in multiple ways. We therefore review some of the most important known facts about strength and prove some new ones. In particular, we present a number of equivalent characterizations of strong functor and strong monad, and give some conditions that guarantee existence or uniqueness of strengths. We look at strength from three different perspectives: actions of a monoidal category V, enrichment over V, and powering over V. We are primarily motivated by semantics of effects, but the results are also useful in other contexts.

Galois connecting callbyvalue and callbyname.
Dylan McDermott and Alan Mycroft.
FSCD 2022. doi:10.4230/LIPIcs.FSCD.2022.32
local PDF, slidesabstract
We establish a general framework for reasoning about the relationship between callbyvalue and callbyname.
In languages with sideeffects, callbyvalue and callbyname executions of programs often have different, but related, observable behaviours. For example, if a program might diverge but otherwise has no sideeffects, then whenever it terminates under callbyvalue, it terminates with the same result under callbyname. We propose a technique for stating and proving these properties. The key ingredient is Levy's callbypushvalue calculus, which we use as a framework for reasoning about evaluation orders. We construct maps between the callbyvalue and callbyname interpretations of types. We then identify properties of sideeffects that imply these maps form a Galois connection. These properties hold for some sideeffects (such as divergence), but not others (such as mutable state). This gives rise to a general reasoning principle that relates callbyvalue and callbyname. We apply the reasoning principle to example sideeffects including divergence and nondeterminism.

Sweedler theory of monads.
Dylan McDermott, Exequiel Rivas, and Tarmo Uustalu.
FoSSaCS 2022. doi:10.1007/9783030992538_22
local PDF, slidesabstract
Monadcomonad interaction laws are a mathematical concept for describing communication protocols between effectful computations and coeffectful environments in the paradigm where notions of effectful computation are modelled by monads and notions of coeffectful environment by comonads. We show that monadcomonad interaction laws are an instance of measuring maps from Sweedler theory for duoidal categories whereby the final interacting comonad for a monad and a residual monad arises as the Sweedler hom and the initial residual monad for a monad and an interacting comonad as the Sweedler copower. We then combine this with a (co)algebraic characterization of monadcomonad interaction laws to derive descriptions of the Sweedler hom and the Sweedler copower in terms of their coalgebras resp. algebras.

Abstract clones for abstract syntax.
Nathanael Arkor and Dylan McDermott.
FSCD 2021. doi:10.4230/LIPIcs.FSCD.2021.30
local PDFabstract
We give a formal treatment of simple type theories, such as the simplytyped λcalculus, using the framework of abstract clones. Abstract clones traditionally describe firstorder structures, but by equipping them with additional algebraic structure, one can further axiomatize secondorder, variablebinding operators. This provides a syntaxindependent representation of simple type theories. We describe multisorted secondorder presentations, such as the presentation of the simplytyped λcalculus, and their clonetheoretic algebras; free algebras on clones abstractly describe the syntax of simple type theories quotiented by equations such as β and ηequality. We give a construction of free algebras and derive a corresponding induction principle, which facilitates syntaxindependent proofs of properties such as adequacy and normalization for simple type theories. Working only with clones avoids some of the complexities inherent in presheafbased frameworks for abstract syntax.

Degrading lists.
Dylan McDermott, Maciej Piróg, and Tarmo Uustalu.
PPDP 2020. doi:10.1145/3414080.3414084
local PDF, slides, Haskell codeabstract
We discuss the relationship between monads and their known generalisation, graded monads, which are especially useful for modelling computational effects equipped with a form of sequential composition. Specifically, we ask if a graded monad can be extended to a monad, and when such a degrading is in some sense canonical. Our particular examples are the graded monads of lists and nonempty lists indexed by their lengths, which gives us a pretext to study the space of all (nongraded) monad structures on the list and nonempty list endofunctors. We show that, in both cases, there exist infinitely many monad structures. However, while there are at least two ways to complete the graded monad structure on lengthindexed lists to a monad structure on the list endofunctor, such a completion for nonempty lists is unique.

Extended callbypushvalue: reasoning about effectful programs and evaluation order.
Dylan McDermott and Alan Mycroft.
ESOP 2019. doi:10.1007/9783030171841_9
Winner of EAPLS Best Paper Award.
local PDF, slidesabstract
Traditionally, reasoning about programs under varying evaluation regimes (callbyvalue, callbyname etc.) was done at the metalevel, treating them as term rewriting systems. Levy's callbypushvalue (CBPV) calculus provides a more powerful approach for reasoning, by treating CBPV terms as a common intermediate language which captures both callbyvalue and callbyname, and by allowing equational reasoning about changes to evaluation order between or within programs.
We extend CBPV to additionally deal with callbyneed, which is nontrivial because of shared reductions. This allows the equational reasoning to also support callbyneed. As an example, we then prove that callbyneed and callbyname are equivalent if nontermination is the only sideeffect in the source language.
We then show how to incorporate an effect system. This enables us to exploit static knowledge of the potential effects of a given expression to augment equational reasoning; thus a program fragment might be invariant under change of evaluation regime only because of knowledge of its effects.

Factorisation systems for logical relations and monadic lifting in typeandeffect system semantics.
Ohad Kammar and Dylan McDermott.
MFPS 2018. doi;10.1016/j.entcs.2018.11.012
local PDF, slidesabstract
Typeandeffect systems incorporate information about the computational effects, e.g., state mutation, probabilistic choice, or I/O, a program phrase may invoke alongside its return value. A semantics for typeandeffect systems involves a parameterised family of monads whose size is exponential in the number of effects. We derive such refined semantics from a single monad over a category, a choice of algebraic operations for this monad, and a suitable factorisation system over this category. We relate the derived semantics to the original semantics using fibrations for logical relations. Our proof uses a folklore technique for lifting monads with operations.

Callbyneed effects via coeffects.
Dylan McDermott and Alan Mycroft.
Open Computer Science, 2018. doi:10.1515/comp20180009
local PDFabstract
Effect systems refine types with information about the behaviour of programs. They have been used for many purposes, such as optimizing programs, determining resource usage, and finding bugs. So far, however, work on effect systems has largely concentrated on callbyvalue languages.
We consider the problem of designing an effect system for a lazy language. This is more challenging because it depends on the ability to locate the first use of each variable. Coeffect systems, which track contextual requirements of programs, provide a method of doing this. We describe how to track variable usage in a coeffect system that can be instantiated for different reduction strategies, including callbyneed. We then add effects to the result, allowing work that has been done on effect systems for callbyvalue languages to be applied to lazy languages.

Project Snowflake: Nonblocking Safe Manual Memory Management in .NET.
Matthew Parkinson, Dimitrios Vytiniotis, Kapil Vaswani, Manuel Costa, Pantazis Deligiannis, Dylan McDermott, Aaron Blankstein, and Jonathan Balkind.
OOPSLA 2017. doi:10.1145/3141879
local PDFabstract
Garbage collection greatly improves programmer productivity and ensures memory safety. Manual memory management on the other hand often delivers better performance but is typically unsafe and can lead to system crashes or security vulnerabilities. We propose integrating safe manual memory management with garbage collection in the .NET runtime to get the best of both worlds. In our design, programmers can choose between allocating objects in the garbage collected heap or the manual heap. All existing applications run unmodified, and without any performance degradation, using the garbage collected heap. Our programming model for manual memory management is flexible: although objects in the manual heap can have a single owning pointer, we allow deallocation at any program point and concurrent sharing of these objects amongst all the threads in the program. Experimental results from our .NET CoreCLR implementation on realworld applications show substantial performance gains especially in multithreaded scenarios: up to 3x savings in peak working sets and 2x improvements in runtime.
PhD thesis

Reasoning about effectful programs and evaluation order.
Submitted October 2019.
thesis
Some talks
There is also a more complete list.

Flexible presentations of graded monads.
Shinya Katsumata, Dylan McDermott, Tarmo Uustalu, and Nicolas Wu.
ICFP 2022, Ljubljana, Slovenia.
slides 
Galois connecting callbyvalue and callbyname.
Dylan McDermott and Alan Mycroft.
FSCD 2022, Haifa, Israel.
slides 
Canonical gradings of monads.
Flavien Breuvart, Dylan McDermott, and Tarmo Uustalu.
ACT 2022, Glasgow, UK.
slides 
Higherorder algebraic theories.
Nathanael Arkor and Dylan McDermott.
Partout seminar, LIX, Paris (online), May 2022.
slides 
Flexible presentations of graded monads.
Shinya Katsumata, Dylan McDermott, Tarmo Uustalu, and Nicolas Wu.
MSP101 seminar, University of Strathclyde (online), April 2022.
slides 
Sweedler theory of monads.
Dylan McDermott, Exequiel Rivas, and Tarmo Uustalu.
FoSSaCS 2022, Munich, Germany.
slides 
What makes a strong monad?
Dylan McDermott and Tarmo Uustalu.
MSFP 2022, Munich, Germany.
slides