Contents

# Contents

## Idea

In type theory, type checking refers to the problem whether the judgment $\Gamma\vdash a \colon A$ is derivable in a given type theory.

## Properties

### Decidability

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.

## References

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