diff --git a/common/header.tex b/common/header.tex
index 0e60363..d95fdf6 100644
--- a/common/header.tex
+++ b/common/header.tex
@@ -81,12 +81,14 @@
   slash-symbol = \sslash{}
 }
 \newcommand{\ofTypeP}[2]{\UseCollection{xfrac}{plainmath}\sfrac{#1}{#2}}
+\newcommand{\matchType}[1]{\Lbag #1 \Rbag}
 
 \newcommand{\Γ}{\Gamma}
 \newcommand{\τ}{\ensuremath{\tau}}
 \newcommand{\σ}{\sigma}
+\DeclareMathOperator\any{\textsc{Any}}
 \newcommand{\λ}{\lambda}
 \newcommand{\recleq}{\sqsubsetleq}
-\newcommand{\discrete}[2]{\left\{ #1, \ldots{}, #2 \right\}}
+\newcommand{\discrete}[2]{\left\{ #1, .., #2 \right\}}
 
 \newcommand{\pref}[1]{\ref{#1} at page~\pageref{#1}}
diff --git a/typing/type-system.tex b/typing/type-system.tex
index 63c5f37..706be77 100644
--- a/typing/type-system.tex
+++ b/typing/type-system.tex
@@ -1,5 +1,49 @@
+\subsection{The $\λ\&-calculus$}
+
+\subsubsection{Patterns}
+
+The typing of patterns is inspired by~\cite{Fri04}: To every pattern $p$,
+we associate a type $\Lbag p \Rbag$ which represents the type of all the
+values accepted by the pattern. The exact definition of $\Lbag \_ \Rbag$ is
+given in figure~\pref{typing::pattern-accept}.
+
+We also define the matching $\ofTypeP{p}{\τ}$ of a type $\τ$ against a pattern
+$p$ (in figure~\pref{typing::pattern-ty-match}).
+
 The typing rules are given by the figures~\pref{typing::lambda-calculus},~\pref{typing::records} and~\pref{typing::operators}.
 
+\begin{figure}
+  \begin{align*}
+    \matchType{x} &= \any \\
+    \matchType{q@x} &= \matchType{q} \\
+    \matchType{\{ f_1, \cdots, f_n \}} &= \{ \matchType{f_1}; \cdots \matchType{f_n}; \} \\
+    \matchType{l} &= l : \any \\
+    \matchType{l ? e} &= l : \any \vee \undef \\
+    \matchType{\text{Cons}(x_1, x_2)} &= \text{Cons}(\any, \any)
+  \end{align*}
+  \caption{Semantics of the $\matchType{\_}$ operator%
+  \label{typing::pattern-accept}}
+\end{figure}
+ii\begin{figure}
+  \begin{align*}
+    \ofTypeP{x}{\τ} &= \sfrac{x}{\τ} &\\
+    \ofTypeP{q@x}{\τ} &= \sfrac{x}{\τ}; \ofTypeP{q}{x} &\\
+    \ofTypeP{\{\}}{\{ x_1 ? c_1, \cdots, x_n ? c_n \}} &=%
+      \sfrac{x_1}{\mathcal{B}(c_1)}; \cdots; \sfrac{x_n}{\mathcal{B}(c_n)} &\\
+    \ofTypeP{\{ s_1 = \τ_1; \cdots; s_m = \τ_m; \}}{\{x_1 ? c_1, \cdots, x_n ? c_n, \textbf{\ldots}\}} &=%
+      \sfrac{x_1}{\mathcal{B}(c_1)}; \cdots; \sfrac{x_n}{\mathcal{B}(c_n)} &%
+        \text{ if } \forall (i,j) \in \discrete{1}{m} \times \discrete{1}{n}, s_i \neq s_j\\
+    \ofTypeP{\{ s = \τ;\}}{\{ x \}} &= \sfrac{x}{\τ}; &\text{ if $s$ = $x$} \\
+    \ofTypeP{\{ s = \τ;\}}{\{ x ? c \}} &= \sfrac{x}{\τ}; &\text{ if $s$ = $x$} \\
+    \ofTypeP{\{ s_1 = \τ_1; \cdots; s_n = \τ_n \}}{\{ x, f_1, \cdots, f_m \}} &=%
+      \sfrac{x}{\τ}; \ofTypeP{\{ s_2 = \τ_2; \cdots; s_n = \τ_n \}}{\{ f_1, \cdots, f_m \}} &\text{ if $s_1$ = $x$} \\
+    \ofTypeP{\{ s_1 = \τ_1; \cdots; s_n = \τ_n \}}{\{ x ? c, f_1 \cdots, f_m \}} &=%
+      \sfrac{x}{\τ}; \ofTypeP{\{ s_2 = \τ_2; \cdots; s_n = \τ_n \}}{\{ f_1, \cdots, f_m \}} &\text{ if $s_1$ = $x$} \\
+    \ofTypeP{\text{Cons}(\τ_1, \τ_2)}{\text{Cons}(x_1, x_2)} &= \sfrac{x_1}{\τ_1}; \sfrac{x_2}{\τ_2} &\\
+  \end{align*}
+  \caption{Semantics of $\ofTypeP{p}{\τ}$%
+  \label{typing::pattern-ty-match}}
+\end{figure}
 \begin{figure}
   \input{typing/lambdaCalculus}
   \caption{Typing rules for the $\λ\&-calculus$\label{typing::lambda-calculus}}