Related papers: Quadratic type checking for objective type theory
We report on the development of an optimized and verified decision procedure for orthologic equalities and inequalities. This decision procedure is quadratic-time and is used as a sound, efficient and predictable approximation to classical…
We contribute XTT, a cubical reconstruction of Observational Type Theory which extends Martin-L\"of's intensional type theory with a dependent equality type that enjoys function extensionality and a judgmental version of the unicity of…
Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality are based on a confluent,…
We define a logical framework with singleton types and one universe of small types. We give the semantics using a PER model; it is used for constructing a normalisation-by-evaluation algorithm. We prove completeness and soundness of the…
We present a general and user-extensible equality checking algorithm that is applicable to a large class of type theories. The algorithm has a type-directed phase for applying extensionality rules and a normalization phase based on…
We prove normalization for MTT, a general multimodal dependent type theory capable of expressing modal type theories for guarded recursion, internalized parametricity, and various other prototypical modal situations. We prove that deciding…
In proof theory the notion of canonical proof is rather basic, and it is usually taken for granted that a canonical proof of a sentence must be unique up to certain minor syntactical details (such as, e.g., change of bound variables). When…
This paper improves the treatment of equality in guarded dependent type theory (GDTT), by combining it with cubical type theory (CTT). GDTT is an extensional type theory with guarded recursive types, which are useful for building models of…
The usual homogeneous form of equality type in Martin-L\"of Type Theory contains identifications between elements of the same type. By contrast, the heterogeneous form of equality contains identifications between elements of possibly…
This is an introductory textbook to univalent mathematics and homotopy type theory, a mathematical foundation that takes advantage of the structural nature of mathematical definitions and constructions. It is common in mathematical practice…
This dissertation gives an overview of Martin Lof's dependant type theory, focusing on its computational content and addressing a question of possibility of fully canonical and computable semantic presentation.
Homotopy type theory is an interpretation of Martin-L\"of's constructive type theory into abstract homotopy theory. There results a link between constructive mathematics and algebraic topology, providing topological semantics for…
Pure type systems arise as a generalisation of simply typed lambda calculus. The contemporary development of mathematics has renewed the interest in type theories, as they are not just the object of mere historical research, but have an…
With the wide range of quantum programming languages on offer now, efficient program verification and type checking for these languages presents a challenge -- especially when classical debugging techniques may affect the states in a…
${\rm CTT}_{\rm qe}$ is a version of Church's type theory that includes quotation and evaluation operators that are similar to quote and eval in the Lisp programming language. With quotation and evaluation it is possible to reason in ${\rm…
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 reduction-free, in the sense of yielding a bijection…
We define a computational type theory combining the contentful equality structure of cartesian cubical type theory with internal parametricity primitives. The combined theory supports both univalence and its relational equivalent, which we…
A wide range of intuitionistic type theories may be presented as equational theories within a logical framework. This method was formulated by Per Martin-L\"{o}f in the mid-1980's and further developed by Uemura, who used it to prove an…
Cubical type theory is an extension of Martin-L\"of type theory recently proposed by Cohen, Coquand, M\"ortberg and the author which allows for direct manipulation of $n$-dimensional cubes and where Voevodsky's Univalence Axiom is provable.…
We propose an abstract notion of a type theory to unify the semantics of various type theories including Martin-L\"{o}f type theory, two-level type theory and cubical type theory. We establish basic results in the semantics of type theory:…