Research
Flow Typing: A New Lens on Linearity
Sky Wilshaw and Graham Hutton. Submitted for publication, 2026. (PDF, Appendix)
Linear type systems often suffer from a threading problem: if a value is used more than once, then it must be explicitly threaded through each usage. Existing solutions introduce extra language features to mitigate this, but at the cost of complicating the core language and its semantics. This article introduces flow typing, a new solution to the threading problem that avoids the need to extend the core language. Flow typing is based on the theory of lenses, a functional presentation of mutable references, in which lens terms mutate parts of a stateful typing context in a controlled way. Because this approach is purely functional, it can be implemented in a standard linear lambda calculus, providing flow typing with a simple and direct semantics.
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.