Research
A Compositional Semantics for Explicit Naming
Sky Wilshaw and Graham Hutton. Submitted for publication, 2025. (PDF)
Accepted to TYPES 2025: extended abstract, slides, video
Naming enables values to be shared between different parts of a computation. We study a notion of explicit naming, where names are first-class citizens, and explicit primitives are provided for creating, using and freeing names. Operationally, such primitives provide a form of manual memory management using pointers. Using this interpretation, we can define a simple semantics for explicit naming by threading through a heap that maps names to values. However, this leads to a non-compositional semantics, which complicates inductive reasoning. To address this, we introduce a lambda calculus with explicit naming, and develop a compositional semantics for it that is provably equivalent to its non-compositional counterpart.
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.