On a Modal λ-Calculus for S4

Abstract

We present λ→□, a concise formulation of a proof term calculus for the intuitionistic modal logic S4 that is well-suited for practical applications. We show that, with respect to provability, it is equivalent to other formulations in the literature, sketch a simple type checking algorithm, and prove subject reduction and the existence of canonical forms for well-typed terms. Applications include a new formulation of natural deduction for intuitionistic linear logic, modal logical frameworks, and a logical analysis of staged computation and binding-time analysis for functional languages [6].