# Chapter 17. Type Theory

Type theory studies formal systems in which expressions are classified by types, and it provides a foundation where logical propositions, mathematical objects, and computational programs can be treated in one unified language.

The chapter begins with simple type theory, where each term has a fixed type and functions are assigned types describing the kinds of inputs they accept and the kinds of outputs they produce.

Dependent types are then introduced, allowing types to depend on terms, so that more precise mathematical statements can be expressed directly inside the formal language.

The Curry-Howard correspondence is studied as the connection between logic and computation, where propositions correspond to types and proofs correspond to terms inhabiting those types.

Proof assistants are then discussed as practical systems based on type theory, where definitions, theorems, and proofs can be checked by a computer according to precise formal rules.

The final part of the chapter introduces formalized mathematics, where large bodies of mathematical knowledge are developed inside proof assistants, making proof verification explicit and mechanically checkable.