A completeness result for the simply typed \(\lambda \mu \)-calculus (Q732057)

The terms of the \(\lambda\)-\(\mu\)-calculus represent the proofs of theorems of classical implicational logic, which are types of these theorems, just as terms of the \(\lambda\)-calculus represent proofs of their types which are theorems of intuitionistic implicational logic. In this paper, a realizability semantics is defined for the simply typed \(\lambda\)-\(\mu\)-calculus. This semantics is shown to be complete using a term model. In addition, for a term \(e\) of type \(\bot \to X\) or \(((X \to \bot)\to X)\to X\), the terms to which \((\dots((e x) y_1) \dots y_n)\) can reduce are found.