natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
XTT is an set-level cubical type theory developed by Jonathan Sterling, Carlo Angiuli, and Daniel Gratzer. While it might seem that XTT should stand for “X type theory”, the authors have stated that XTT isn’t an acronym and doesn’t stand for anything.
XTT features boundary separation, which implies UIP as a theorem of XTT, rather than an axiom as in Martin-Löf type theory. As a result, it is an example of a cubical type theory which is not a homotopy type theory.
Additionally, XTT has regularity, canonicity, and certain higher inductive types like propositional truncation. It is an open question if it additionally has decidable type checking and normalization.
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer, Cubical syntax for reflection-free extensional equality. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), volume 131 of Leibniz International Proceedings in Informatics (LIPIcs), pages 31:1-31:25. (arXiv:1904.08562, doi:10.4230/LIPIcs.FCSD.2019.31)
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer, A Cubical Language for Bishop Sets, Logical Methods in Computer Science, 18 (1), 2022. (arXiv:2003.01491).
Last revised on September 4, 2022 at 21:36:39. See the history of this page for a list of all contributions to it.