Alex Rice

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
GitHub https://github.com/alexarice
Orcid 0000–0002–2698–5122

About Me

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

Posters

Talks

Posts

Teaching

Events

I have attended the following events: