A revised completeness result for the simply typed $\lambda\mu$-calculus using realizability semantics

TL;DR

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

Contribution

It provides a revised realizability semantics for the simply typed lambda-mu-calculus and corrects previous errors in related work.

Findings

Typable terms inhabit their type interpretation

Established a completeness result using a specific term model

Corrected earlier errors in the semantics

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.