Research

A Compositional Semantics for Explicit Naming

Sky Wilshaw and Graham Hutton. In preparation, 2025.

Accepted to TYPES 2025: extended abstract

Naming enables values to be shared between different parts of a computation. We focus on a notion of explicit naming, where names are first-class citizens, with explicit primitives for creating, using and freeing names. Operationally, such primitives can be viewed as providing a form of manual memory management using pointers. Indeed, the traditional approach to defining a semantics for explicit naming involves 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 that is provably equivalent to its non-compositional counterpart.

New Foundations is consistent

M. Randall Holmes and Sky Wilshaw. In preparation, 2025.

arXiv, Homepage, GitHub

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.