Daniel Marshall

a.k.a. starsandspirals

email: daniel@starsandspira.ls
twitter: @starsandspirals
cv: pdf

Hi! I'm currently pursuing an EPSRC-funded PhD in the Programming Languages and Systems group at the University of Kent, working on the Granule project. I previously studied for a four-year integrated MComp degree in Computer Science with Mathematics at the University of Sheffield. I'm particularly interested in functional programming, language design and implementation, category theory and mathematical logic.

fun facts:

publications

How to Take the Inverse of a Type (pearl)
Daniel Marshall, Dominic Orchard
to appear in ECOOP 2022 [draft] [artifact]
in summary: It is well-known that regular types form a semiring, with product types for multiplication. But is there any way we can divide one type by another? It turns out that if your types are linear, then there is a way. We explore this idea and look at some interesting applications such as stencil computations.

Linearity and Uniqueness: An Entente Cordiale
Daniel Marshall, Michael Vollmer, Dominic Orchard
ESOP 2022 [paper] [slides] [artifact]
in summary: Are linearity and uniqueness the same concept? Are they somehow "dual" to one another? This paper answers these questions and resolves the confusion once and for all. We develop a calculus for linear and unique types in a single system, and provide a practical implementation in Granule.

Replicate, Reuse, Repeat:
Capturing Non-Linear Communication via Session Types and Graded Modal Types
Daniel Marshall, Dominic Orchard
PLACES 2022 [paper] [slides] [erratum]
in summary: Session types are closely related to linear logic, but being able to represent non-linear behaviours while preserving some of the safety properties ensured by linearity can often be useful. We show how to represent some such behaviours in a precise way by using graded modal types.

Linearity, Uniqueness, Ownership: An Entente Cordiale
Daniel Marshall
first place at POPL 2022 SRC [extended abstract] [virtual poster]

Linear Exponentials as Graded Modal Types
Jack Hughes, Daniel Marshall, James Wood, Dominic Orchard
TLLA 2021 [extended abstract]
in summary: Graded type systems generalise linear types by letting us talk about resources in a more fine-grained way. But can we really model linear logic inside the graded world? We enrich our system with an additional operation to make sure that in Granule, we definitely can.

undergrad

My undergraduate project on program verification.

My Darwin (master's) project was on comparing evolutionary algorithms for solving the graph colouring problem, working in a group with three other fourth year students and supervised by Dr. Dirk Sudholt. We implemented a framework using DEAP for running different variants of evolutionary algorithms on different graph classes, and compared the performance of state-of-the-art evolutionary algorithms like the hybrid colouring algorithm against simple theory-driven evolutionary algorithms.

My undergraduate project (pdf) was on verifying the correctness of functional programs using Isabelle/HOL. I was supervised by Prof. Georg Struth. I began by proving statements about simple functional data structures like natural numbers, lists, and trees, moved on to verifying the correctness of simple sorting algorithms like insertion sort and merge sort, and finally implemented a definition of the shuffle product operation on strings and languages, providing proofs of some known properties from the literature.

Before I started university I did my A-Levels at Longley Park Sixth Form, where I achieved an A* in Mathematics and 3 As in Further Mathematics, Physics and Chemistry. I also worked on an extended project discussing the mathematics of artificial intelligence and the ways that computers can make decisions, for which I was also given an A* grade. Prior to that I did my GCSEs at Firth Park Academy.

experience

Me presenting at BCUR 2019.

Over the summer of 2019 I worked on a Google Summer of Code project (details), mentored by Chris Smith and Daniel Cartwright. I created a GHC plugin which allows instructors to define requirements for the code within a project and automatically validate them, with applications for users in a broad range of educational contexts. It offers validation of requirements from basic static analysis like checks for line length and warnings through to more advanced testing like template matching.

Earlier that summer I did some research (pdf) with Jordan Williamson, a PhD student working in algebraic topology. I learned the basics of category theory and commutative algebra, and studied Morita theory, which allows us to learn about rings by examining their module categories. We managed to show some interesting results relating to torsion modules.

In the summer of 2018 I worked with Pete Dodd and Mozhgan Kabiri Chimeh as part of the Sheffield Undergraduate Research Experience program. I used data collected from Zambia and South Africa and applied the agent-based modelling tool FLAME GPU to create a model of tuberculosis transmission that runs around 30x faster than a comparable model running on a single core. I presented these results in April 2019 at the British Conference of Undergraduate Research in Pontypridd.

More contrast
Dark mode