I am currently a postdoctoral research assistant working with Chris Heunen on methods of representing quantum programs which makes them easier to optimise, write, or reason about. I have previously worked with Tobias Grosser, and did my PhD at the University of Cambridge under the supervision of Jamie Vicary.
Contact
Email
alex.rice at ed.ac.uk
Office Address
Office 3.05 Informatics Forum University of Edinburgh Edinburgh EH8 9AB United Kingdom
I am generally interested at the moment in all things related to programming languages and type systems, and tools for working with these. In my PhD, I developed two variants of the type theory Catt, a type theory which models globular weak infinity categories. These variants had added definitional equality allowing them to model semistrict infinity categories. During this I generated an interpreter for these languages, and formalised a substantial portion of their metatheory in Agda.
I also enjoy formalising things in Agda, programming in rust, and am a user of Emacs and the NixOS Linux distribution. My other interests include ice skating/ice hockey and playing cello in orchestras.
Thesis
My thesis “thesis”, was submitted on 18th April 2024 (pdf, arxiv)
Papers
“Quantum Circuits are Just a Phase” with Chris Heunen, Christopher McNally, and Louis Lemonnier, POPL 2026 (pdf, arxiv, doi)
“A Syntax for Strictly Associative and Unital ∞-Categories” with Eric Finster and Jamie Vicary, LICS 2024 (pdf, arxiv, doi)
“A Type Theory for Strictly Unital ∞-Categories” with Eric Finster, David Reutter, and Jamie Vicary, LICS 2022 (pdf, arxiv, doi)
“A Type Theory for Strictly Associative Infinity Categories” with Eric Finster and Jamie Vicary (pdf, arxiv)
“New minimal linear inferences in Boolean logic independent of switch and medial” with and Anupam Das, extended version in LMCS (pdf, arxiv, lmcs), original version at FSCD 2021 (pdf, link)
