Seminari del Dipartimento


Logica e Informatica Teorica

Toward a denotational semantics for proofs in constructive modal logic

Daniele Catta

12-03-2021 - 15:00
modalitĂ  telematica (telematic form)


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)
org: PEDICINI Marco

Copyright© 2014 Dipartimento di Matematica e Fisica