About me

I'm a PhD student in the Functional Programming Lab in the University of Nottingham. In 2024, I graduated from the Cambridge Mathematical Tripos.

My research focuses on the semantics of borrowing, a language feature allowing a logical resource to be loaned out by its owner. Loaned variables can be used immutably in a variety of ways, but these loans may expire at some point in the program, allowing the original owner to reclaim unique ownership. This paradigm has been used extensively by languages like Rust and Austral. I'm researching what borrowing is and why it works, at an abstract level.

Publications

0009-0004-2439-3459

In preparation	•	A Compositional Semantics for Explicit Naming
		Sky Wilshaw and Graham Hutton
In preparation	•	New Foundations is consistent
		M. Randall Holmes and Sky Wilshaw
		arXiv, Homepage, GitHub

Talks

2025	•	Compositional memory management in the λ-calculus
		Sky Wilshaw and Graham Hutton
		TYPES 2025: extended abstract
2024	•	New Foundations: the story of a large formalisation project
		Sky Wilshaw
		Cambridge Lean User Group. Birmingham Theory Group.

Links