Research
Flow Typing for Lightweight Linearity
Sky Wilshaw and Graham Hutton. In preparation.
Linear types are useful for writing safe resource-sensitive programs, but a strict linearity discipline is too burdensome to uphold in practice. To make linearity practical, languages often add extra typing features such as borrowing, but such features complicate the semantics and can be challenging to use. In this paper, we introduce flow typing as an alternative approach. Flow typing allows us to write linear code in a natural and familiar style, but has a simple semantics via a translation into a linear lambda calculus. We introduce and implement our ideas using a Haskell-like language that is compiled down to Linear Haskell.
A Compositional Semantics for Explicit Naming
Sky Wilshaw and Graham Hutton. Submitted for publication, 2026. (PDF)
Accepted to TYPES 2025: extended abstract, slides, video
Names are ubiquitous in programming. This article considers a notion of explicit naming, where names are first-class citizens, and explicit primitives are provided for creating, using and freeing names. We present two semantics for explicit naming. The first is a traditional imperative semantics that threads a heap mapping names to values. The second is an alternative functional semantics that uses effects to track name manipulation compositionally, without explicit state passing. To relate the two, we employ clairvoyant semantics, a technique that allows us to “look into the future” of a computation. We show that clairvoyance provides a natural bridge between the functional and imperative perspectives, enabling a proof of their equivalence.
New Foundations is consistent
M. Randall Holmes and Sky Wilshaw. Submitted for publication, 2025. (PDF)
In this paper we will present a proof of the consistency of Quine's set theory “New Foundations” (hereinafter NF), so-called after the title of the 1937 paper in which it was introduced. This version takes the approach of building a model of tangled type theory rather than a model of the usual set theory without choice with a tangled web of cardinals; further, details of the construction are refined due to interaction with the now complete verification in Lean by the second author.