**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 $\Gamma\vdash a \colon A$ 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.

- Martin Hofmann,
*Extensional concepts in intensional type theory*, Ph.D. dissertation, University of Edinburgh (1995). (link)

See also:

- Wikipedia,
*Type system*

Created on June 19, 2022 at 03:55:14. See the history of this page for a list of all contributions to it.