About

Hi, I'm Nathan. I'm currently reading for a DPhil in Computer Science at the University of Oxford. I was previously an undergraduate at the University of Cambridge and remain a visiting member of the Cambridge Logical Structures Hub. Broadly speaking, my research interests lie in Programming Language Theory; Type Theory; Category Theory; and Compiler Construction. I am also a member of the Frex Project.

Beyond the realm of 1s and 0s, I enjoy bouldering, music, strategy games and cryptic crosswords.

Writing

Frex: Dependently Typed Algebraic Simplification

[bib|pdf|arXiv]

Guillame Allais, Edwin Brady, Nathan Corbyn, Ohad Kammar and Jeremy Yallop

Proceedings of the ACM on Programming Languages, Volume 9, Issue ICFP (ICFP 2025)

homotopy.io: A Proof Assistant for Finitely-Presented Globular n-Categories

[bib|pdf|arXiv]

Nathan Corbyn, Lukas Heidemann, Nick Hu, Chiara Sarti, Calin Tataru and Jamie Vicary

9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Generalised free extensions

[bib|pdf|poster]

Nathan Corbyn

Extended abstract (2022)

Normalization by Evaluation with Free Extensions

[bib|pdf|talk]

Nathan Corbyn, Ohad Kammar, Sam Lindley, Nachiappan Valliappan and Jeremy Yallop

Extended abstract (2022)

Proof synthesis with free extensions in intensional type theory

[bib|pdf]

Nathan Corbyn

Master's dissertation (2021)

Practical static memory management

[bib|pdf]

Nathan Corbyn

Bachelor's dissertation (2020)

Talks

Understanding the Classical Monad-Theory Correspondence

[slides]

Invited speaker

July 2024 — 10th Workshop on Mathematically Structured Functional Programming (MSFP 2024)

Generalised free extensions

[slides|video]

September 2022 — ICFP'22 student research competition

You might not need your garbage collector**

[slides|video]

June 2022 — Huawei-Edinburgh Joint Lab

Code

homotopy-io/homotopy-rs

homotopy.io is a web-based proof assistant, built to support a theory of finitely presented globular n-categories. I played an active role in the development of the tool's latest incarnation, focusing primarily on the interface and graphics code. Most substantially, I worked on enabling real-time rendering of 4D surface diagrams as animations.

cofibrant/micro-mitten

micro-mitten is a bare-bones Rust-like programming language, developed for my undergraduate dissertation. It uses a memory-management strategy called ASAP (Proust, 2017) to permit full compile-time garbage collection without introducing regions or ownership.

rust-lang/rust

I made several contributions to the Rust compiler. Most of this work was connected with the stabilisation of async/await.

Contact

The best way to contact me is by email at [me@nathancorbyn.com].