Most programming languages exhibit a phase distinction between the static and dynamic phases of processing, where the first phase involves type checking used to ensure that program is well-formed and the second one consists of execution of such well-formed programs. As aforementioned, a PL is safe exactly when all well-formed programs are well-behaved when executed.

As such, the static phase contains a set of rules for deriving typing judgements stating that an expression is well-formed of a certain type, which somehow “predicts” the behavior of the program when it runs. Type safety tells us that these predictions are correct; otherwise, the statics is considered to be mal-formed, resulting in an unsafe language for execution.

Personal notes:

• Syntax defines the appearance of a target language.
• Semantics defines the inductive rule.
• Recall again what mathematical induction means. To prove a property $P$ holds, we need to prove: 1) $P(0)$ holds, and 2) $n \in \mathbb{N}, P(n) \Rightarrow P(n+1).$ There is also structural induction where we need to prove the derivation rule.

Syntax

Undoubtedly, the first thing one needs to do is define the abstract syntax of the target language. For the sake of clarity, it is recommended that we first define minimal concrete syntax conventions to avoid the bothering of complex syntax. This books starts with a simple language called $\sf E$.

$$ \begin{align*} \mathsf{Type} \quad \tau ::= \quad &\mathtt{num} \quad \mathtt{num}\\ & \mathtt{str} \quad \mathtt{str} \\ \mathsf{Expr} \quad e ::= \quad &x \quad x \\ &num[n] \quad n \\ &str[s] \quad ``s" \\ &\mathtt{plus}(e_1;e_2) \quad e_1 + e_2 \\ & \mathtt{times}(e_1;e_2) \quad e_1 * e_2 \\ &\cdots \\ &\end{align*} $$

The syntax usually has a category, an abstract form and a concret form. The above syntax defines two sorts, $\sf Type$ ranged over $\tau$, and $\sf Expr$, ranged over by $e$.

Type System

Type system is used to impose restrictions on the formations of phrases that are sensitive to the context where they occur. The statics of $\bf E$ consists of an inductive definition of generic hypothetical jdugments of the form

$$ \mathcal{X} \mid \Gamma \vdash e: \tau, $$

where $\cal X$ is a finite set of variables, and $\Gamma$ is a typing context consisting of hypotheses of the form $x: \tau$, one for each $x \in \cal X$. For example, we may have a rule:

$$ \overline{\Gamma, x: \tau \vdash x: \tau}. $$

Additionally, we write $x \notin \mathsf{Dom}(\Gamma)$ to say that there is no assumption in $\Gamma$ of the form $x : \tau$ for any type. This is to prevent naming conflicts.