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

Sean Walsh

A system ${\mathbf{\lambda }}_{\theta }$ is developed that combines modal logic and simply-typed lambda calculus, and that generalizes the system studied by Montague and Gallin. Whereas Montague…