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
In type theory, type checking refers to the problem whether the judgment is derivable in a given type theory.
For instance, intensional type theory has decidable type checking, but extensional type theory, which adds the rule of equality reflection, does not. For an exposition of this result, see Hofmann 1995.
In more expressive type theories, we can also ask whether judgmental equality (also called computational or definitional equality) is decidable. Since deciding the judgmental equality is often a prerequisite for deciding type checking, systems with decidable type checking often have decidable judgmental equality.
See also:
Created on June 19, 2022 at 03:55:14. See the history of this page for a list of all contributions to it.