In this paper we investigate the Curry-Howard 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 and we prove normalization and confluence for our calculus. We then provide a typing system in the style of focused proof systems allowing us to provide a unique proof for each term in normal form, and we use this result to show a one-to-one correspondence between terms in normal form and winning innocent strategies.

翻译：本文探讨了构造性模态逻辑的Curry-Howard对应关系，重点研究了文献中λ演算所施加的证明等价关系与近期针对该逻辑定义的获胜策略之间的差距。我们通过为文献中的演算增加额外的归约规则，定义了一个适用于最小构造性模态逻辑的新λ演算，并证明了该演算的规范化与合流性。随后，我们采用聚焦证明系统风格的类型系统，为每个范式项提供了唯一证明，并利用这一结果证明了范式项与获胜无辜策略之间的一一对应关系。