nLab Mitchell Riley

Selected writings

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

Selected writings

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

On adjoint logic:

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

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]

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

Proof that Conway's game of life is omniperiodic:

A modal type theory for tiny objects:

category: people

Last revised on March 5, 2024 at 14:53:58. See the history of this page for a list of all contributions to it.