A revised completeness result for the simply typed $\lambda\mu$-calculus using realizability semantics
Logic
2023-06-22 v4 Logic in Computer Science
Abstract
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.
Keywords
Cite
@article{arxiv.1612.09223,
title = {A revised completeness result for the simply typed $\lambda\mu$-calculus using realizability semantics},
author = {Karim Nour and Mohamad Ziadeh},
journal= {arXiv preprint arXiv:1612.09223},
year = {2023}
}
Comments
arXiv admin note: text overlap with arXiv:0905.0357