Towards a denotational semantics for proofs in constructive modal logic

Davide CATTA
12/03/2021 - 15:00
Online su Teams

Venerdì 12 marzo 2021 alle ore 15:00, si terrà il seminario del dott. Daniele Catta (Université di Montpellier)
dal titolo "Toward a denotational semantics for proofs in constructive modal logic".


Constructive modal logics are extensions of intuitionistic propositional logic with certain modal axioms. Many
proof systems are known for these logics, but the only available denotational semantics is defined by means
of an abstract construction, based on the quotient of their lambda terms.

The general aim of our work is to define a game semantics for constructive modal logics. In this talk, I will define
the winning strategies for a formula and show the correspondence between winning strategies and proofs. I will
show how winning strategies can be defined as the projection of specific paths in a graphical proof system
defined for this purpose - combinatorial proofs.

(This talk is based on joint work with Matteo Acclavio and Lutz Straßburger)

Per partecipare al seminario cliccare sul seguente Link