Mitchell Riley

I am a postdoc at NYU Abu Dhabi, working under Hisham Sati and Urs Schreiber. My mathematical interests include (homotopy) type theory, applied category theory, and more generally anything at the interface of mathematics and computers.

Contact

Dissertation

Projects

at: Effective Algebraic Topology in Haskell

A Haskell rewrite of Kenzo, a collection of algorithms for explicit constructions with simplicial sets. Currently capable of computing 𝜋₄ S³ and the homology of K(Z/m,n), among other things.

Symmetric CatForce

A search program for interesting patterns in Conway's Game of Life, written in C++. Similar to ptbsearch but much faster. Has been used to find a huge number of interesting oscillators.

Originally based on CatForce, but very little original code remains.

Papers and Preprints

7. A Type Theory with a Tiny Object,
   2024.
   [arXiv:2403.01939]
6. Conway's Game of Life is Omniperiodic,
   with Nico Brown, Carson Cheng, Tanner Jacobi, Maia Karpovich, Matthias Merzenich and David Raucci.
   2023.
   [arXiv:2312.02799] [quanta]
5. Commuting Cohesions,
   with David Jaz Myers.
   2023.
   [arXiv:2301.13780]
4. A Dependent Bunched Type Theory for Synthetic Stable Homotopy Theory,
   with Dan Licata.
   2022.
   In preparation.
3. Synthetic Spectra via a Monadic and Comonadic Modality,
   with Eric Finster and Dan Licata.
   2021.
   [arXiv:2102.04099]
2. Categories of Optics,
   2018.
   [arXiv:1809.00738]
1. A Fibrational Framework for Substructural and Modal Logics,
   with Dan Licata and Mike Shulman.
   FSCD, 2017.
   [short pdf] [extended pdf]

Notes

• A Whirlwind Tour of Combinatorial Games in Haskell, 2014.
  [literate haskell]

Talks

• Commuting Cohesions. HoTT 2023, May 2023.
  [slides]
• Combining Bunched Type Theory with Dependent Types. Atlantic Category Theory Seminar, February 2022.
  [slides]
p
• Linear Homotopy Type Theory. HoTTEST Event for Junior Researchers, January 2022.
  [slides] [video]
• Constructive Mathematics for People Who Aren't Not Normal. Wesleyan Graduate Student Seminar, November 2021.
• Using Linear Homotopy Type Theory Informally. CMU, October 2021.
  [slides]
• Good Categories with Bad Objects. Wesleyan Graduate Student Seminar, September 2021.
• Extending Homotopy Type Theory with Linear Type Formers. CCS Colloquium, Augusta University, March 2021.
  [slides] [video]
• A Type Theory for Parameterised Spectra. ICMS Session on Univalent Mathematics, July 2020.
  [slides]
• Synthetic Spectra via a Monadic and Comonadic Modality. HoTTEST Conference, June 2020.
  [slides] [video]
• A Type Theory for Parameterised Spectra, focusing on the type theory. CMU, March 2020.
  [slides]
• A Type Theory for Parameterised Spectra, starting from scratch, no type theory background. Wesleyan University, February 2020.
  [slides]
• Combinatorial Game Theory. Wesleyan Graduate Student Seminar, November 2019.
• Categories of Optics, MIT (Applied) Categories Seminar, May 2019.
  [video]
• Yoneda Arises Everywhere. Wesleyan Graduate Student Seminar, January 2019.
• Exact Real Arithmetic in Haskell, Brisbane Functional Programming Group, May 2015.
  [video] [code]

Reviewing

Teaching

• Spring 2022: TA for COMP301, Automata Theory and Formal Languages
• Fall 2021: TA for COMP321, Principles of Programming Languages
• Spring 2021: TA for COMP212, Functional Programming
• Fall 2020: TA for COMP301, Automata Theory and Formal Languages
• Spring 2020: TA for COMP212, Functional Programming
• Fall 2020: TA for COMP301, Automata Theory and Formal Languages
• Spring 2019: Lecturer for MATH120, Elements of Calculus, Part II
• Fall 2018: TA for COMP112, Introduction to Programming
• Spring 2018: Lecturer for MATH118, Introductory Calculus II: Integration and Its Applications
• Spring 2017: TA for COMP312, Algorithms and Complexity
• Fall 2016: TA for COMP211, Computer Science I