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 “A type-theoretic approach to semistrict higher categories”, was submitted on 18th April 2024 (pdf, arxiv)
Papers
Quantum Circuits are Just a Phase, POPL 2026 (pdf, arxiv, doi)
A Syntax for Strictly Associative and Unital ∞-Categories, LICS 2024 (pdf, arxiv, doi)
A Type Theory for Strictly Unital ∞-Categories, LICS 2022 (pdf, arxiv, doi)
A Type Theory for Strictly Associative Infinity Categories (pdf, arxiv)
New minimal linear inferences in Boolean logic independent of switch and medial, extended version in LMCS (pdf, arxiv, lmcs), original version at FSCD 2021 (pdf, link)
