Type systems help to apply and check for a syntactically consistent interpretation. They rule out programs that do not make any sense and allow certain operations while disallowing others.

Typing Relations

The Typing Relation for arithmetic expressions is the smallest binary relation between terms and types satisfying all instances of the typing rules.

A term \(t\) is typable or well-typed if there is some \(T\) such that \(t:T\).

Soundness

If \(K \vdash P\) then \(K \vDash P\) in \(T\).

If the conclusion is provable from the premise, then the premise logically entails the conclusion.

Progress

A well-typed term \(t\) is not stuck.

If \(t : T\) then either \(t\) is a value or \(t \to t^\prime\) for some \(t^\prime\)

Preservation

Types are preserved by one-step evaluation

If \(t:T\) and \(t \to t^\prime\) then \(t^\prime : T\)

Simply-Typed Lambda Calculus

Annotating terms

\(x\) is of type \(T\) is denoted as \begin{equation} \lambda x:T.t \end{equation} The type depends on the context.