Lax modal lambda calculi

Abstract: Intuitionistic modal logic (IML) is the study of extending intuitionistic propositional logic with modal operators such as the box and diamond modalities. Advances in IML have led to a plethora of useful applications in programming languages via the development of corresponding type theories with modalities. Until recently, IMLs with diamonds had been misunderstood as somewhat peculiar and unstable, causing the development of type theories with diamonds to lag behind type theories with boxes.

In this talk, I will present 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 strong functors in functional programming and make it possible to formalize the connection between possible-world semantics for IMLs and categorical semantics for corresponding lambda calculi. I hope to end this talk with a summary of what I’ve learnt from IML literature and how it has inspired me to think about semantics of modalities in programming languages beyond boxes and diamonds.

A draft article on this topic can be found here: $\url{https://nachivpn.me/lmlc.pdf}$

computer science theoryMathematics

Audience: researchers in the topic

University of Birmingham theoretical computer science seminar

Series comments: Meeting ID: 818 7333 5084 ~ Password: 217