Realizability Interpretation and Normalization of Typed Call-by-Need $$\lambda$$-calculus With Control

Étienne Miquey, Hugo Herbelin

We define a variant of realizability where realizers are pairs of a term and a substitution. This variant allows us to prove the normalization of a simply-typed call-by-need $$λ$-$…