The Many Worlds of Modal λ-calculi: I. Curry-Howard for Necessity, Possibility and Time

Abstract

This is a survey of λ-calculi that, through the Curry-Howard isomorphism, correspond to constructive modal logics. We cover the prehistory of the subject and then concentrate on the developments that took place in the 1990s and early 2000s. We discuss logical aspects, modal λ-calculi, and their categorical semantics. The logics underlying the calculi surveyed are constructive versions of K, K4, S4, and LTL.

References in corpus (2)

• Logical Relations for Monadic Types
• Calculi for Intuitionistic Normal Modal Logic

Cited by in corpus (5)

• Intensionality, Intensional Recursion, and the Gödel-Löb axiom
• Fitch-Style Modal Lambda Calculi
• Logic of computational semi-effects and categorical gluing for equivariant functors
• Categorical and Algebraic Aspects of the Intuitionistic Modal Logic ${\mathrm{IEL}}^{-}$ and its predicate extensions
• Modality via Iterated Enrichment