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. We also prove a completeness result of our realizability semantics using a particular term model. This paper corrects some errors in [21] by the first author and Saber.Comment: arXiv admin note: text overlap with arXiv:0905.0357

@article{NourZ16,
  title = {A revised completeness result for the simply typed $\lambda\mu$-calculus using realizability semantics},
  author = {Karim Nour and Mohamad Ziadeh},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 13, Issue 3},
  year = {2017},
  doi = {10.23638/lmcs-13(3:13)2017}
}