I am studying at the University of Cambridge after completing the first year of my PhD at the University of Birmingham. I am working under the supervision of Jamie Vicary.
|alex.rice at cl.cam.ac.uk|
|Office Address||Office FS35
The Computer Laboratory
University of Cambridge
William Gates Building
My main interests at the moment are type theory, including Homotopy Type Theory, and its applications to higher category theory. I am currently looking at various definitions of globular higher categories and am thinking about semi-strictness problems and types of composition.
Before starting my PhD I completed a 4-year integrated masters program in Mathematics and Computer Science at the University of Oxford. During this time I took courses including Category Theory (including theory of monoidal categories), Algebraic Topology, Homological Algebra, Logic, ZFC Set Theory, and Representation Theory.
I also enjoy formalising things in Agda and and am a user of Emacs and the NixOS Linux distribution.
- Strictly Associative and Unital ∞-Categories as a Generalized Algebraic Theory (pdf, arxiv)
- 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)
- 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)
- 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 assistant for “Advanced Functional Programming” (Autumn 2019)
- Teaching assistant for “Logic and Computation” (Spring 2019)
- Supervisor for “Semantics of Programming Languages” (Autumn 2020)
- Supervisor for “Prolog” (Spring 2021, Spring 2022, and Spring 2023)
- Supervisor for “Introduction to Probability” (Summer 2021)
- Supervisor for “Object Oriented Programming” (Autumn 2021)
I have attended the following events: