@inproceedings{eb8b34f01fa64f0db99cb6d788059dab,
title = "Canonicity of Proofs in Constructive Modal Logic",
abstract = "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.",
keywords = "Constructive Modal Logic, Game Semantics, Lambda Calculus",
author = "Matteo Acclavio and Davide Catta and Federico Olimpieri",
note = "Funding Information: The first author is supported by Villum Fonden, grant no. 50079. The second author is supported by the PRIN project RIPER (No. 20203FFYLK) The third author is supported by the US Air Force Office for Scientific Research under award number FA9550-21-1-0007.; 32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2023 ; Conference date: 18-09-2023 Through 21-09-2023",
year = "2023",
doi = "10.1007/978-3-031-43513-3_19",
language = "English",
isbn = "9783031435126",
series = "Lecture Notes in Computer Science",
publisher = "Springer Science+Business Media",
pages = "342--363",
editor = "Revantha Ramanayake and Josef Urban",
booktitle = "Automated Reasoning with Analytic Tableaux and Related Methods - 32nd International Conference, TABLEAUX 2023, Proceedings",
address = "United States",
}