Lax Modal Lambda Calculi

TL;DR

This paper introduces a family of typed lambda calculi based on Lax logic, providing a modal foundation for strong functors in programming, with formal semantics and proof of key properties.

Contribution

It develops new typed lambda calculi for Lax logic with formal semantics and proofs, advancing understanding of diamonds in intuitionistic modal logics.

Findings

Constructed categorical and possible-world semantics.

Proved normalization and completeness.

Formalized results in Agda.

Abstract

Intuitionistic modal logics (IMLs) extend intuitionistic propositional logic with modalities such as the box and diamond connectives. Advances in the study of IMLs have inspired several applications in programming languages via the development of corresponding type theories with modalities. Until recently, IMLs with diamonds have been misunderstood as somewhat peculiar and unstable, causing the development of type theories with diamonds to lag behind type theories with boxes. In this article, we develop a family of typed-lambda calculi corresponding to sublogics of a peculiar IML with diamonds known as Lax logic. These calculi provide a modal logical foundation for various strong functors in typed-functional programming. We present possible-world and categorical semantics for these calculi and constructively prove normalization, equational completeness and proof-theoretic inadmissibility results. Our main results have been formalized using the proof assistant Agda.