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

G. A. Kavvos

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 th…