nLab Mitchell Riley

Mitchell Riley is postdoctoral researcher at CQTS @ NYU Abu Dhabi.

• institute page at NYU Abu Dhabi

• old institute page at Iowa

Selected writings

The Kenzo-program for constructive algebraic topology (computational topology) re-written in Haskell:

• Mitchell Riley: github.com/mvr/at

On adjoint logic:

• Daniel Licata, Mike Shulman, and Mitchell Riley, A Fibrational Framework for Substructural and Modal Logics (extended version), in Proceedings of 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) (doi: 10.4230/LIPIcs.FSCD.2017.25, pdf)

On optics (in computer science), such as lenses:

• Mitchell Riley, Categories of optics [arXiv:1809.00738, video:YT]

On homotopy dependent linear type theory of dependent stable homotopy types (via a form of bunched logic) with categorical semantics in parametrized spectra:

• Mitchell Riley, Eric Finster, Daniel Licata, Synthetic Spectra via a Monadic and Comonadic Modality [arXiv:2102.04099]

• Mitchell Riley, Extending Homotopy Type Theory with Linear Type Formers, talk at The ForML LAb (2021) [web, video]

• Mitchell Riley, A Bunched Homotopy Type Theory for Synthetic Stable Homotopy Theory, PhD Thesis (2022) [doi:10.14418/wes01.3.139, ir:3269, pdf]

• Mitchell Riley, Linear Homotopy Type Theory, talk at: HoTTEST Event for Junior Researchers 2022 (Jan 2022) [slides: pdf, pdf, video: YT]

  Abstract. Some ∞-toposes support constructions that are inherently ‘linear’, such as the external smash product of parameterised spectra. These cannot be added axiomatically to ordinary HoTT, because there is no way to enforce this linearity: there are no restrictions on variable uses. This talk describes an extension of HoTT with linear tensor and hom type formers, as a kind of ‘binary modality’ and its right adjoint. Trying to stay compatible with existing results in HoTT naturally leads us to a novel kind of bunched dependent type theory. Our type theory is intended to be as human-usable as possible, with an eye towards synthetic stable homotopy theory.

• Mitchell Riley, Dependent Type Theories à la Carte, talk at CQTS Initial Researcher’s Meeting (Sep 2022) [pdf]

• Mitchell Riley, A Linear Dependent Type Theory with Identity Types as a Quantum Verification Language (2023) [pdf, pdf]

  (translation between LHoTT and the proto-Quipper of Fu, Kishida & Selinger 2020)

On cohesive homotopy type theory with a pair of commuting cohesive structures (such as for differential orbifold cohomology):

• David Jaz Myers, Mitchell Riley, Commuting Cohesions [arXiv:2301.13780]

Proof that Conway's game of life is omniperiodic:

• Nico Brown, Carson Cheng, Tanner Jacobi, Maia Karpovich, Matthias Merzenich, David Raucci, Mitchell Riley, Conway’s Game of Life is Omniperiodic [arXiv:2312.02799]

• The Physics arXiv Blog, Mathematicians Prove the “Omniperiodicity” of Conway’s Game of Life (Dec 2024)

A modal type theory for tiny objects:

• Mitchell Riley, A Type Theory with a Tiny Object [arXiv:2403.01939]

• Mitchell Riley: Tiny Objects in Type Theory, talk at Running HoTT 2024, CQTS @ NYU Abu Dhabi (Apr 2024) [slides:pdf, video: kt]

category: people