Normalization by realizability also evaluates

For those of us that generally live in the world of syntax, semantic proof techniques such as realizability or logical relations/parametricity sometimes feel like magic. Why do they work? At which point in the proof is “the real work” done? Bernardy and Lasson [4] express realizability and parametricity models as syntactic models - but the abstraction/adequacy theorems are still explained as meta-level proofs. Hoping to better understand the proof technique, we look at those proofs as programs themselves. How does a normalization argument using realizability actually computes those normal forms? This detective work is at an early stage and we propose a first attempt in a simple setting. Instead of arbitrary Pure Type Systems, we use the simply-typed lambda-calculus.