Simply typed lambda calculus, \(\lambda^\to\).

\[ \mathcal{S} = \star, \square \qquad \mathcal{A} = \star : \square \qquad \mathcal{R} = (\star, \star, \star) \]

>>> prettyPut $ specificationDoc STLCStar
𝓢: ⋆, □
𝓐: ⋆ : □
𝓡: (⋆,⋆,⋆)

System F, \(\lambda2\).

\[ \mathcal{S} = \star, \square \qquad \mathcal{A} = \star : \square \qquad \mathcal{R} = (\star, \star, \star), (\square, \star, \star) \]

>>> prettyPut $ specificationDoc SysFStar
𝓢: ⋆, □
𝓐: ⋆ : □
𝓡: (⋆,⋆,⋆), (□,⋆,⋆)

Hindley-Milner as PTS.

HindleyMilner is a truncated MartinLof: with only two universes.

\[ \mathcal{S} = M, P \qquad \mathcal{A} = M : P \qquad \mathcal{R} = (M,M,M), (P,M,P), (P,P,P) \]

>>> prettyPut $ specificationDoc HMMono
𝓢: M, P
𝓐: M : P
𝓡: (M,M,M), (P,M,P), (P,P,P)

Calculus of Constructions, \(\lambda C\).

\[ \mathcal{S} = \star, \square \qquad \mathcal{A} = \star : \square \qquad \mathcal{R} = (\star, \star, \star), (\square, \star, \star), (\star, \square, \square), (\square, \square, \square) \]

>>> prettyPut $ specificationDoc CoCStar
𝓢: ⋆, □
𝓐: ⋆ : □
𝓡: (⋆,⋆,⋆), (⋆,□,□), (□,⋆,⋆), (□,□,□)

Martin-Löf type system.

\[ \mathcal{S} = \mathbb{N} \qquad \mathcal{A} = n : n + 1; n \in \mathbb{N} \qquad \mathcal{R} = (n, m, \max n\, m); n, m \in \mathbb{N} \]

>>> prettyPut $ specificationDoc (star_ :: MartinLof)
𝓢: 𝓤, 𝓤₁, 𝓤₂
𝓐: 𝓤 : 𝓤₁, 𝓤₁ : 𝓤₂, 𝓤₂ : 𝓤₃
𝓡: (𝓤,𝓤,𝓤),
   (𝓤,𝓤₁,𝓤₁),
   (𝓤₁,𝓤,𝓤₁),
   (𝓤₁,𝓤₁,𝓤₁),
   (𝓤,𝓤₂,𝓤₂),
   (𝓤₂,𝓤,𝓤₂),
   (𝓤₁,𝓤₂,𝓤₂),
   (𝓤,𝓤₃,𝓤₃),
   (𝓤₃,𝓤,𝓤₃), ...

λHOL

\[ \begin{align} \mathcal{S} &= \star, \square, \triangle \newline \mathcal{A} &= \star : \square, \square : \triangle \newline \mathcal{R} &= (\star, \star, \star), (\square, \star, \star), (\square, \square, \square), (\triangle, \star, \star) \end{align} \]

The $(triangle, star, star)$ is an extension rule.

>>> prettyPut $ specificationDoc HOLStar
𝓢: ⋆, □, △
𝓐: ⋆ : □, □ : △
𝓡: (⋆,⋆,⋆), (□,⋆,⋆), (□,□,□), (△,⋆,⋆)

\(\lambda^\star\) system.

Inconsistent.

\[ \mathcal{S} = \star \qquad \mathcal{A} = \star : \star \qquad \mathcal{R} = (\star, \star, \star) \]

>>> prettyPut $ specificationDoc LambdaStar
𝓢: ⋆
𝓐: ⋆ : ⋆
𝓡: (⋆,⋆,⋆)

System U, \(\lambda U\).

Inconsistent.

\[ \begin{align} \mathcal{S} &= \star, \square, \triangle \newline \mathcal{A} &= \star : \square, \square : \triangle \newline \mathcal{R} &= (\star, \star, \star), (\square, \star, \star), (\square, \square, \square), (\triangle, \star, \star), (\triangle, \square, \square) \end{align} \]

>>> prettyPut $ specificationDoc SysUStar
𝓢: ⋆, □, △
𝓐: ⋆ : □, □ : △
𝓡: (⋆,⋆,⋆), (□,⋆,⋆), (□,□,□), (△,⋆,⋆), (△,□,□)