A completeness result for the simply typed λμ-calculus
classification
🧮 math.LO
keywords
resulttypedcalculuscompletenesslambdarealizabilitysemanticssimply
read the original abstract
In this paper, we define a 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. 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.