Invited Talks

Alessio Guglielmi (University of Bath): Concerto pour une Voix (Joint work with Chris Barrett and Victoria Barrett)

Abstract: Subatomic proof systems in deep inference exploit the idea that atoms can be seen as superpositions of values, for example, true and false. Adopting this point of view leads to some dramatic simplifications of proof systems and their proof theory, and this talk provides an example. A single, simple, linear inference shape, together with a certain notion of saturation, generates a proof system for a language of standard boolean operators augmented by decision trees. We prove cut-elimination and several other proof-theoretic results for this proof system. Moreover, the proof system provides cut-free proofs of Statman tautologies that are polynomial in the size of the tautologies, while standard proof systems only yield exponential cut-free proofs. The ideas are natural, simple, and mostly rely on two notions that appear to have very general applicability: projecting proofs around atoms and eversion of formulae. More information about deep inference is at http://alessio.guglielmi.name/res/cos/.

Dale Miller (Inria Saclay - Île-de-France and the Laboratoire d'Informatique (LIX)): Contexts in sequents as indexed storage

Abstract: By examining focused proof systems for classical and intuitionistic logics, it is natural to see the contexts used to build sequents as indexed storage devices. More precisely, a context is a relation between formulas and indexes. Depending on the nature of such indexes, sequent calculus proofs can be used to accommodate structures such as Tseitin constants, De Bruijn indexes, subformula occurrences, etc. I will cover the motivations for this approach to contexts as well as illustrate several applications of it.

Valeria de Paiva (Topos Institute): Constructive Modalities

Abstract: Modalities (temporal, epistemic, deontic, etc) have proved themselves extremely useful in theoretical computer science, multi-agent systems and AI, usually in the setting of classical logic. Recently there seems to be a renewed interest in the notions of constructive (or intuitionistic) modal type theory and linear type theory, in part because of the interest in homotopy type theory. Since I have been working on modal extensions of the Curry-Howard correspondence to logical systems since the 90s, it seems a good idea to recap some of the old ideas associated with modal type theory. Especially because it seems to me that there are plenty of old problems that have not been solved, yet.

Elaine Pimentel (University of Rio Grande de Norte): Hypersequent calculi for non-normal modal and deontic logics

Abstract: In this talk, we will present a gentle introduction to hypersequents for systems of the classical cube and some extensions. Such calculi are internal, as they only employ the language of the logic, plus additional structural connectives. By showing a translation between hypersequent rule applications and derivations in a labelled system, we will explain the differences and similarities between internal and external calculi for the classical cube. Finally, we will show a terminating proof search strategy in the hypersequent calculi, where from every failed proof of a formula or hypersequent it is possible to directly extract a countermodel out of it. This is a joint work with Tiziano Dalmonte, Nicola Olivetti and Björn Lellmann.