A completeness result for the simply typed $\lambda\mu$-calculus

TL;DR

This paper introduces a realizability semantics for the simply typed λμ-calculus, establishing that typable terms inhabit their type interpretations and providing a completeness result through a specific term model.

Contribution

It presents a novel realizability semantics for the simply typed λμ-calculus and proves a completeness theorem using a specialized term model.

Findings

Typable terms inhabit their type interpretation

Semantics characterizes computational behavior of closed typed terms

Completeness established via a specific term model

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.