We prove the conjecture that any Grothendieck $(\infty, 1) $-topos can be presented by a
Quillen model category that interprets homotopy type theory with strict univalent universes …

We introduce MTT, a dependent type theory which supports multiple modalities. MTT is
parametrized by a mode theory which specifies a collection of modes, modalities, and …

We combine homotopy type theory with axiomatic cohesion, expressing the latter internally
with a version of 'adjoint logic'in which the discretization and codiscretization modalities are …

We prove normalization for (univalent, Cartesian) cubical type theory, closing the last major
open problem in the syntactic metatheory of cubical type theory. Our normalization result is …

We present a graded modal type theory, a dependent type theory with grades that can be
used to enforce various properties of the code. The theory has Π-types, weak and strong Σ …

We prove normalization for MTT, a general multimodal dependent type theory capable of
expressing modal type theories for guarded recursion, internalized parametricity, and …

We report on the development of the HoTT library, a formalization of homotopy type theory in
the Coq proof assistant. It formalizes most of basic homotopy type theory, including …

The theory of program modules is of interest to language designers not only for its practical
importance to programming, but also because it lies at the nexus of three fundamental …

Higher inductive types are a class of type-forming rules, introduced to provide basic (and not-
so-basic) homotopy-theoretic constructions in a type-theoretic style. They have proven very …

We present calf, ac ost-a ware l ogical f ramework for studying quantitative aspects of
functional programs. Taking inspiration from recent work that reconstructs traditional aspects …