A completeness result for the simply typed $\lambda\mu$-calculus
Logic
2009-05-05 v1
Abstract
In this paper, we define a realizability semantics for the simply typed -calculus. We show that if a term is typable, then it inhabits the interpretation of its type. This result serves to give characterizations of the computational behavior of some closed typed terms. We also prove a completeness result of our realizability semantics using a particular term model.
Keywords
Cite
@article{arxiv.0905.0357,
title = {A completeness result for the simply typed $\lambda\mu$-calculus},
author = {Karim Nour and Khelifa Saber},
journal= {arXiv preprint arXiv:0905.0357},
year = {2009}
}