Sean Walsh

Simply-typed constant-domain modal lambda calculus I: distanced beta reduction and combinatory logic

2026 · Logical Methods in Computer Science

A system $\boldsymbolλ_θ$ is developed that combines modal logic and simply-typed lambda calculus, and that generalizes the system studied by Montague and Gallin. Whereas Montague and Gallin worked with Church's simple theory of types, the …