A revised completeness result for the simply typed $\lambda \mu$-calculus using realizability semantics

Karim Nour, Mohamad Ziadeh

In this paper, we define a new realizability semantics for the simply typed lambda-mu-calculus. We show that if a term is typable, then it inhabits the interpretation of its type.…