Program &
Accepted Papers

Model Comparison Game and n-Bisimulation for Conditional Logic

by Xiaoxuan Fu (China🇨🇳) and Zhiguang Zhao (China🇨🇳)

Marianna Girlando (Invited Talk)

Cyclic proofs for Transitive Closure Logic via Hypersequents

Propositional Dynamic Logic (PDL) is a modal logic for reasoning about the iterative execution of programs. Via the standard translation, PDL can be embedded into Transitive Closure Logic (TCL), an extension of first-order logic with a recursive operator expressing the transitive closure of binary relations. Cyclic proof systems based on Gentzen-style sequents have been developed for both PDL and TCL in the literature, but cyclic proofs for PDL do not directly translate into cyclic proofs for TCL. Therefore, the standard translation does not lift to the level of Gentzen-style cyclic proofs. Motivated by this observation, we introduce a hypersequent-style cyclic proof system for TCL, which enriches Gentzen-style sequents with additional structural connectives. We prove that this system is sound and that it simulates cyclic proofs for PDL, thereby establishing cut-free completeness for a fragment of TCL. This talk is based on joint work with Anupam Das: https://link.springer.com/article/10.1007/s10817-023-09675-1

A Circuit-Theoretic View of FO over Semirings

by Timon Barlag (Germany🇩🇪), Nicolas Fröhlich (Germany🇩🇪), Teemu Hankala (Estonia🇪🇪), Miika Hannula (Estonia🇪🇪), Minna Hirvonen (Germany🇩🇪), Vivian Holzapfel (Germany🇩🇪), Juha Kontinen (Finland🇫🇮), Arne Meier (Germany🇩🇪) and Laura Strieker (Germany🇩🇪)

Shadowy Institutions

by Siddharth Bhaskar (Denmark🇩🇰) and Robin Kaarsgaard (Denmark🇩🇰)

Knowledge and Common Knowledge of Strategies

by Borja Sierra Miranda (Switzerland🇨🇭) and Thomas Studer (Switzerland🇨🇭)

Possible and impossible conditionals for team logics

by Fausto Barbero (Finland🇫🇮) and Fan Yang (the Netherlands🇳🇱)

Axiomatizing Eventual Common Knowledge

by Roman Kuznets (Czechia🇨🇿), Rojo Randrianomentsoa (Switzerland🇨🇭) and Thomas Studer (Switzerland🇨🇭)

An Axiomatization of Büchi Arithmetic

by Konstantin Kovalyov (Russia🇷🇺)

Two generalizations of shininess

by Guilherme V. Toledo (Brazil🇧🇷) and Yoni Zohar (Israel🇮🇱)

Decidability of MSO Reparametrization over Countable Labelled Chain

by Alexander Rabinovich (Israel🇮🇱)

Delia Kesner (Invited Talk)

Quantitative Types

Quantitative techniques are emerging in different areas of computer science in response to the growing need to reason about resource-aware computation. This talk introduces quantitative types, a mathematical framework that provides a unified understanding of resource usage in higher-order programming languages. We first present the key ideas underlying quantitative types, from both computational and semantic perspectives. We then show how these systems can be applied to quantitatively characterize normalization, solve inhabitation problems, and study observational equivalence.