For closed terms u, and type 𝜏 we are going to define u ⊩ 𝜏 (read “u is a realiser of 𝜏”). Let's say that we have PCF's type: ℕ and σ → τ.

1. u ⊩ ℕ if u reduces to a natural number literal
2. f ⊩ σ → τ if for all s⊩σ, f s ⊩ τ.

Some immediate observations:

• This definition is by induction on the types, and assumes little from the terms (it's a logical relation).
• This is “really what we mean” by x : 𝜏 (except non-termination, not modelled here): realisability has explanatory power.
• This relation is usually undecidable.
• It is strongly related to parametricity (in parametricity we associate a binary relation to types, in realisability we associate a (unary) predicate). 4/10
• From this point of view, typing is a (usually decidable) modular approximation of realisability.
• For instance, consider if x then 1 else (\y -> y). It isn't well-typed.
• However, if we add let x = True in if x then 1 else (λy. y) it becomes a realiser of ℕ [because upon reduction, it produces an N, even though it is not "well-typed".

• Typing and realisability are related by a lemma sometimes referred as adequacy.

Take the rule for λ (simplified):

x:X, y:Y ⊢ z : Z-----------------------x:X ⊢ λ(y: Y). z : Y → Z

You interpret it as a statement

∀ v⊩A, (∀ w ⊩ B, u[x\v, y\w] ⊩ C) ⟹  \lambda y.u[x\v] ⊩ C

• Then, you prove this statement. 7/10

Once you've done so for each rule, you can conclude (very easy induction) that if ⊢ u : A, then u ⊩ A. This gives type safety, since realisers are practically defined as verifying type safety.

What you've gained along the way is that this proof is an open induction. 8/10

In standard combinatorial proofs of type safety, the induction hypothesis may depend on every case. Adding a form in your language may require redoing the entire proof. Here the various case in the adequacy lemma will remain true. So you can just prove the new cases. 9/10

There are many variants of realisability. Tuned for logic, with models instead of terms, … My favourite is Krivine's realisability with both terms and stacks, and magic happening when they interact. But this is another story and shall be told another time. 10/10