Canonicity in Modal Lambda Calculus

In this paper we investigate the Curry-Howard-Lambek correspondence for constructive modal logic in light of the gap between the proof equivalences enforced by the lambda calculi from the literature and by the recently defined winning strategies for this logic. We define a new lambda-calculus for a minimal constructive modal logic by enriching the calculus from the literature with additional reduction rules. After proving normalization results for our calculus, we provide a typing system in the style of focused proof systems for the terms in normal forms. We conclude by showing the one-to-one correspondence between those terms and winning innocent strategies.