Search

• < Previous
• 1
• Next >

---

Multimodal Dependent Type Theory

Daniel Gratzer ; G. A. Kavvos ; Andreas Nuyts ; Lars Birkedal.

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 transformations between them. We show that different choices of mode theory allow us to use the same type theory to compute and&nbsp;[&hellip;]

---

A Cubical Language for Bishop Sets

Jonathan Sterling ; Carlo Angiuli ; Daniel Gratzer.

We present XTT, a version of Cartesian cubical type theory specialized for Bishop sets \`a la Coquand, in which every type enjoys a definitional version of the uniqueness of identity proofs. Using cubical notions, XTT reconstructs many of the ideas underlying Observational Type Theory, a version of&nbsp;[&hellip;]

---