Avatar

Nathan Corbyn

Oxford, UK

Doctoral Computer Science student at the University of Oxford

About

Hi, I'm Nathan, I'm 24 and 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 and music. I'm also one to dabble in philosophy!

Writing

Generalised free extensions

Nathan Corbyn

(Extended abstract) 2022.

[bibtex][pdf]

Normalization by evaluation with free extensions

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

(Extended abstract) 2022.

[bibtex][pdf]

Frex: dependently-typed algebraic simplification

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

(Draft) 2023.

[bibtex][arXiv]

Proof synthesis with free extensions in intensional type theory

Nathan Corbyn

Master's Thesis 2021

[bibtex][pdf]

Practical static memory management

Nathan Corbyn

Bachelor's Thesis 2020

[bibtex][pdf]

Talks

Generalised free extensions

September 2022 — ICFP'22 student research competition

[slides][video]

You might not need your garbage collector**

June 2022 — Huawei-Edinburgh Joint Lab

[slides][video]

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 play an active role in the development of the tool's latest incarnation, focusing primarily on the interface and graphics code. Most recently, I've been working on enabling real-time rendering of 4D surface diagrams as animations.

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 very occasionally contribute to the Rust compiler. Most of my work so far has been connected with the stabilisation of async/await. I haven't had much time to contribute recently, but I'm hoping to get stuck in again soon.

Contact

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