Alex Rice
I am currently a postdoctoral research assistant working with Chris Heunen and Tobias Grosser on the intersection of programming languages, compilation, and quantum computing. I have just submitted my thesis for a PhD at the University of Cambridge under the supervision of Jamie Vicary.
Contact
| alex.rice at ed.ac.uk | |
| Office Address | Office SE01 The Computer Laboratory University of Cambridge William Gates Building Cambridge CB3 0FD United Kingdom |
| GitHub | https://github.com/alexarice |
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)
Papers
- A Syntax for Strictly Associative and Unital ∞-Categories (pdf, arxiv, doi)
- A Type Theory for Strictly Unital Infinity Categories (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), originally presented at FSCD 2021 (pdf, link)
- Coinductive Invertibility in Higher Categories (pdf, formalisation, github, arxiv)
Talks
- July 2024: A Syntax for Strictly Associative and Unital ∞-Categories, LICS 2024 (slides)
- April 2023: Strictly Associative Group Theory using Univalence, HoTT/UF 2023 (slides)
- December 2022: A Type Theory for Strictly Associative Infinity Categories, SYCO 10 (slides)
- August 2022: A Type Theory for Strictly Unital Infinity Categories, LICS 2022 (slides)
- May 2022: Type theoretic approaches to semistrict higher categories, YAMCATS 27 (slides)
- July 2021: New minimal linear inferences in Boolean logic independent of switch and medial, FSCD 2021 (recording, slides)
- June 2021: Categories and Companions Symposium - Biased composition in infinity categories (recording, slides)
- 25th September 2020: Birmingham theory group lab lunch - Biased composition in infinity categories
- 19th March 2020: Birmingham theory group lab lunch - Coinductive Invertibility in Higher Categories (slides)
Posts
- The Kavvos-Sojakova proof of Syllepsis in Agda
- Linear inferences of size 7 - 09/10/2020
- Strictly Associative Group Theory using Univalence - 29/05/2020
- Strictly Associative Group Theory - 26/03/2020
Teaching
- Guest lecturer for “Advanced Topics in Category Theory” (Spring 2024)
- Supervisor for “Prolog” (Spring 2021, Spring 2022, and Spring 2023)
- Supervisor for “Introduction to Probability” (Summer 2021)
- Supervisor for “Object Oriented Programming” (Autumn 2021)
- Supervisor for “Semantics of Programming Languages” (Autumn 2020)
- Teaching assistant for “Advanced Functional Programming” (Autumn 2019)
- Teaching assistant for “Logic and Computation” (Spring 2019)
Events
I have attended the following events:
- HoTT/UF 2023
- SYCO 11
- SYCO 10
- FLOC 2022 (HoTT/UF, LICS, FSCD)
- YAMCATS 27
- Midlands graduate school (MGS) 2022
- Logic and Higher Structures
- FSCD 2021
- ACT 2021, which I helped organise.
- Categories and Companions Symposium 2021
- SYCO 6
- SYCO 3
- SYCO 2
- MGS Christmas lectures in Sheffield 2019