Volume
LIPIcs, Volume 363
34th EACSL Annual Conference on Computer Science Logic (CSL 2026)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL)
Event
Editors
Publication Details
- published at: 2026-02-18
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-411-6
Access Numbers
- Detailed Access Statistics available here
-
Total Accesses (updated on a weekly basis)
0Documents
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 363, CSL 2026, Complete Volume
Abstract
LIPIcs, Volume 363, CSL 2026, Complete Volume
Cite as
34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 1-958, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Proceedings{guerrini_et_al:LIPIcs.CSL.2026,
title = {{LIPIcs, Volume 363, CSL 2026, Complete Volume}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {1--958},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026},
URN = {urn:nbn:de:0030-drops-254885},
doi = {10.4230/LIPIcs.CSL.2026},
annote = {Keywords: LIPIcs, Volume 363, CSL 2026, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{guerrini_et_al:LIPIcs.CSL.2026.0,
author = {Guerrini, Stefano and K\"{o}nig, Barbara},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {0:i--0:xiv},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.0},
URN = {urn:nbn:de:0030-drops-254870},
doi = {10.4230/LIPIcs.CSL.2026.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Ackermann Award
The Ackermann Award 2025
Abstract
Report on the 2025 Ackermann Award, on behalf of the EACSL Ackermann Award Jury.
Cite as
Maribel Fernández and Prakash Panangaden. The Ackermann Award 2025. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 1:1-1:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{fernandez_et_al:LIPIcs.CSL.2026.1,
author = {Fern\'{a}ndez, Maribel and Panangaden, Prakash},
title = {{The Ackermann Award 2025}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {1:1--1:5},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.1},
URN = {urn:nbn:de:0030-drops-254251},
doi = {10.4230/LIPIcs.CSL.2026.1},
annote = {Keywords: graph transducer, linear dynamical system, model checking problem}
}
Document
Invited Talk
The Logic Behind Colour Refinement (Invited Talk)
Abstract
Colour Refinement is a combinatorial algorithm that computes a vertex colouring for an input graph to reveal its structural properties. Each iteration of the algorithm refines the current colouring by assessing local information. More precisely, the new colour of a vertex is determined by its current colour and the multiset of colours in its neighbourhood. This refinement procedure continues until it reaches a stable partition of the vertex set into colour classes.
On the practical side, the algorithm admits fast implementations. Because the final colouring is isomorphism-invariant, executing the algorithm on two graphs in parallel can be used to demonstrate that they are not isomorphic. From a theoretical perspective, the algorithm is arguably the most straightforward combinatorial approach to detecting asymmetries - specifically for distinguishing vertices that do not belong to the same orbit of the automorphism group of the graph. Its numerous connections to other areas in computer science stand as evidence of its robustness and naturalness and make it a fascinating object of research.
Among the most elegant connections is the link to counting logic. Colour Refinement assigns distinct final colours to two vertices in a graph if and only if there is a formula in the two-variable fragment C² of the logic C that distinguishes them, meaning that the formula holds for precisely one of the two vertices. In fact, the vertex colours translate directly into logical formulas with one free variable. As a consequence, Colour Refinement distinguishes two graphs if and only if there is a C²-sentence that distinguishes them. This correspondence extends to higher dimensions: the k-variable fragment C^k of C corresponds to the (k-1)-dimensional extension of Colour Refinement, the (k-1)-dimensional Weisfeiler-Leman algorithm. This algorithm computes a unique colouring for a graph G if and only if G is definable in C^k, i.e. there is a sentence in C^k whose only models are G and its isomorphic copies.
As a matter of fact, the link to the logic C goes even deeper: the number of Colour Refinement iterations required to compute distinct colours corresponds exactly to the quantifier depth of a distinguishing formula. Since the iterations induce a sequence of strictly nested vertex partitions, the process must terminate after at most n-1 rounds, where n is the number of vertices. Consequently, the value n-1 serves as a trivial upper bound on both the number of iterations and the quantifier depth required to distinguish any two (distinguishable) vertices in C².
My talk provides an introduction to the link between the Colour Refinement procedure and the logic C². We revisit a simple characterisation of their expressivity on graphs and on general relational structures. The characterisation implies that the definability of a graph in C² can be checked very efficiently.
We then discuss tight lower bounds on the quantifier depth of C²-formulas required to distinguish vertices. Through a thorough analysis of computational data from Colour Refinement executions, we constructed infinite families of graphs that witness those bounds. We finish with a presentation of a recent purely theoretical reverse-engineering approach to finding long-refinement graphs and a classification of all such graphs with small (or, equivalently, large) degrees.
The talk is based on the collaborations[Sandra Kiefer and T. Devini de Mel, 2026; Kiefer and McKay, 2020; Sandra Kiefer et al., 2022] and unpublished work.
Cite as
Sandra Kiefer. The Logic Behind Colour Refinement (Invited Talk). In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{kiefer:LIPIcs.CSL.2026.2,
author = {Kiefer, Sandra},
title = {{The Logic Behind Colour Refinement}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {2:1--2:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.2},
URN = {urn:nbn:de:0030-drops-254263},
doi = {10.4230/LIPIcs.CSL.2026.2},
annote = {Keywords: Colour Refinement, counting logic, Weisfeiler-Leman algorithm, variable width, quantifier depth}
}
Document
Invited Paper
Rational Lawvere Logic (Invited Paper)
Abstract
We study Rational Lawvere logic (RL). This logic is defined over the extended positive reals with an algebraic structure combining the Lawvere quantale (with the reversed order on the extended reals and a sum as tensor) and a multiplicative quantale (with the usual order on the extended reals and a multiplication as tensor); together they provide a semiring structure. The logic is designed for complex quantitative reasoning, including sequents expressing inequalities between rational functions over the extended positive reals. We give a deduction system and demonstrate its expressiveness by deriving a classical result from probability theory relating the Kantorovich and total variation distances. Our deductive system is complete for finitely axiomatizable theories. The proof of completeness relies on the Krivine-Stengle Positivstellensatz.
We additionally provide complexity results for both RL and its affine fragment AL. We consider two decision problems: the satisfiability of a set of sequents and whether a sequent follows from a finite set of sequent. We show that both problems lie in PSPACE for RL, and we give sharper complexity bounds for AL: the first problem is NP-complete, while the second is co-NP-complete.
Cite as
Giorgio Bacci, Radu Mardare, Prakash Panangaden, and Gordon Plotkin. Rational Lawvere Logic (Invited Paper). In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 3:1-3:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{bacci_et_al:LIPIcs.CSL.2026.3,
author = {Bacci, Giorgio and Mardare, Radu and Panangaden, Prakash and Plotkin, Gordon},
title = {{Rational Lawvere Logic}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {3:1--3:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.3},
URN = {urn:nbn:de:0030-drops-254277},
doi = {10.4230/LIPIcs.CSL.2026.3},
annote = {Keywords: Quantitative reasoning, complete deductive system, Lawvere’s quantale}
}
Document
Invited Talk
Towards A Rosetta Stone of Interactive and Quantitative Semantics (Invited Talk)
Abstract
Quantitative semantics are those denotational semantics that inherit from linear logic [Jean-Yves Girard, 1987] a sensitivity to the multiplicity of resources involved in computation. Those include the relational model [Jean-Yves Girard, 1987] and its numerous variations (such as finiteness spaces [Thomas Ehrhard, 2005], weighted relational models [Jim Laird et al., 2013] and their extensions [Thomas Ehrhard et al., 2011; Thomas Ehrhard, 2002], generalized species of structure [Fiore et al., 2008], span models [Paul-André Melliès, 2019; Pierre Clairambault and Simon Forest, 2023], etc), as well as related syntactic methods such as non-idempotent intersection types [Daniel de Carvalho, 2018] and Taylor expansion of lambda-terms [Thomas Ehrhard and Laurent Regnier, 2003]. Interactive semantics are usually also quantitative, but in addition they present the interactive behaviour of proofs and programs, generally organized chronologically - those include the many variants of game semantics (starting with [J. M. E. Hyland and C.-H. Luke Ong, 2000; Samson Abramsky et al., 2000]), and other frameworks such as Geometry of Interaction [Girard, 1989] or ludics [Jean-Yves Girard, 2001]. Both families are cornerstones of modern denotational semantics, and both have associated Alonzo Church awards: game semantics in 2017, and quantitative semantics (in particular, differential linear logic and the differential λ-calculus) in 2024.
It has more or less always been clear to the experts that the two, sharing an origin in linear logic, are conceptually related. Yet there are differences, which seem fundamental: in particular, while quantitative models compose relationally, the composition of strategies follows an intricate "parallel interaction plus hiding" process inspired from concurrency theory [Abramsky, 1997]. The two families of models have also historically targeted different kinds of languages: whereas quantitative semantics focused on theoretical calculi (and the λ-calculus in particular), game semantics is known for fully abstract models for languages with elaborate combinations of effects including local state [Samson Abramsky and Guy McCusker, 1996], control operators [James Laird, 1997], and concurrent primitives [Dan R. Ghica and Andrzej S. Murawski, 2008]. Early on, researchers have explored the relationship between the two [Thomas Ehrhard, 1996; Patrick Baillot et al., 1997], and investigations on this question have spanned decades [Pierre Boudes, 2009; Ana C. Calderon and Guy McCusker, 2010; Takeshi Tsukada and C.-H. Luke Ong, 2016; C.-H. Luke Ong, 2017]. In particular, Melliès' work on asynchronous games [Paul-André Melliès, 2006; Paul-André Melliès, 2005] made significant conceptual contributions, showing that the issue was enlightened by adopting a positional formulation of game semantics, where points in the relational model simply arise as certain positions.
This talk surveys recent developments in this line of work, shedding light on the connection between those two families. Our work is set in so-called "thin concurrent games" [Simon Castellan et al., 2019; Pierre Clairambault, 2024], an extension with symmetry of Rideau and Winskel’s concurrent games on event structures [Silvain Rideau and Glynn Winskel, 2011]. Event structures being one of the main "truly concurrent" models of concurrency [Glynn Winskel, 1986], it is perhaps expected that thin concurrent games can model concurrent languages: they provide a truly concurrent refinement of Ghica and Murawski’s fully abstract model of Idealized Concurrent Algol [Simon Castellan and Pierre Clairambault, 2024; Pierre Clairambault, 2024]. But beyond the semantics of concurrency, thin concurrent games are also a deep reworking on game semantics built from causal principles, inheriting from asynchronous games a positional flavour. In thin concurrent games, strategies have a dual nature: an event-based nature where they appear as certain event structures composed via parallel interaction plus hiding; or a positional nature where they appear as certain spans of groupoids, composed by pullback (modulo a technical condition on strategies called visibility) - they can be regarded both as a games and a relational model!
Leveraging this dual nature, in a sequence of papers with Castellan, de Visme, Olimpieri and Paquet, we have been able to link the single framework of thin concurrent games with numerous other models. This includes various traditional alternating or non-alternating games models [Simon Castellan and Pierre Clairambault, 2024; Pierre Clairambault, 2024], the weighted relational model [Pierre Clairambault and Hugo Paquet, 2021], the quantum relational model [Pierre Clairambault and Marc de Visme, 2020], generalized species of structure [Pierre Clairambault et al., 2023], and - going beyond quantitative semantics - the linear Scott model [Clairambault, 2025], a linear decomposition of standard Scott domain semantics [Thomas Ehrhard, 2012]. All these distinct models are obtained by projecting away certain aspects of thin concurrent games, giving some support to the claim that thin concurrent games are a Rosetta stone for interactive and quantitative semantics.
Cite as
Pierre Clairambault. Towards A Rosetta Stone of Interactive and Quantitative Semantics (Invited Talk). In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 4:1-4:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{clairambault:LIPIcs.CSL.2026.4,
author = {Clairambault, Pierre},
title = {{Towards A Rosetta Stone of Interactive and Quantitative Semantics}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {4:1--4:4},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.4},
URN = {urn:nbn:de:0030-drops-254286},
doi = {10.4230/LIPIcs.CSL.2026.4},
annote = {Keywords: Denotational semantics, Game semantics}
}
Document
Invited Talk
Automata and Algebras for Probability and Nondeterminism (Invited Talk)
Abstract
Probabilistic models of computation have been studied for over three decades now, from foundational, logical, coalgebraic, categorical, as well as more practical verification-motivated point of view. In my work, and in this talk, we focus on the foundational, semantics side of probabilistic automata and transition systems, and in particular the relevant monads, and their algebras. The interplay of probability and non-determinism has been particularly challenging from a semantics point of view for some decades, as it does not just yield a monad. There are by now well-studied solutions to this and several monads for probability and non-determinism: some enriching the structure with convexity to obtain a monad, albeit a non-commutative one, others deliberately simplifying it, by imposing commutativity.
It is well known that monads have two faces: a computational one - we think here of the powerset monad modelling non-determinism, or the probability distribution monad modelling probabilistic choices, and a universal-algebraic one - where we think of the algebraic presentation of the monads, like semilattices for the powerset monad and (variants of) convex algebras for (variants of) the probability distribution monad. Combining non-determinism and probability yields other combined monads, among which probably the most studied is the convex-subsets-of-distributions monad. This monad is presented by so-called convex semilattices, algebraic structures that are both a semilattice and a convex algebra, with suitable distributivity connecting the operations.
From a semantics point of view, the algebraic presentations give us a nice way to define (and sometimes compute) language (aka trace) equivalence of the corresponding automata. Moreover, the presentations are useful for axiomatizations of language equivalence. From an algebraic point of view, these algebras are interesting and many questions about them are still open. We will discuss language semantics, its axiomatization, as well as some obtained and open algebraic problems for convex algebras and convex semilattices - and their computational consequences. In particular, we have a full characterization of congruences of (variants of) convex algebras, which for example yields decidability of distribution semantics; other results on congruences, e.g. a result on a congruence being finitely generated as a subalgebra, surprisingly accellerated the proof of completeness of infinite trace semanitcs, etc. We will review some existing results: all congruences are described and fp = fg for convex algebras, termination is a black hole, useful functors are proper on convex algebras, cancellativity of convex semi-lattices; as well as mention ongoing work on: mid-point-cancellativity, subalgebras, and homomorphisms for convex semi-lattices, as well as topological convex semilattices.
This talk is based on previous joint works with Filippo Bonchi, Alexandra Silva, Valeria Vignudelli, and Harald Woracek, as well as on ongoing work and discussions with Matteo Mio, Alex Simpson, and Harald Woracek.
Cite as
Ana Sokolova. Automata and Algebras for Probability and Nondeterminism (Invited Talk). In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, p. 5:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{sokolova:LIPIcs.CSL.2026.5,
author = {Sokolova, Ana},
title = {{Automata and Algebras for Probability and Nondeterminism}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {5:1--5:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.5},
URN = {urn:nbn:de:0030-drops-254295},
doi = {10.4230/LIPIcs.CSL.2026.5},
annote = {Keywords: probabilistic transition systems and automata, Labelled Markov processes, Markov decision processes, convex algebras, convex semilattices, coalgebraic semantics}
}
Document
Hereditary First-Order Logic: the Tractable Quantifier Prefix Classes
Abstract
Many computational problems can be modelled as the class of all finite structures A that satisfy a fixed first-order sentence ϕ hereditarily, i.e., we require that every (induced) substructure of A satisfies ϕ. We call the corresponding computational problem the hereditary model checking problem for ϕ, and denote it by Her(ϕ).
We present a complete description of the quantifier prefixes for ϕ such that Her(ϕ) is in P; we show that for every other quantifier prefix there exists a formula ϕ with this prefix such that Her(ϕ) is coNP-complete. Specifically, we show that if Q is of the form ∀*∃∀* or of the form ∀*∃*, then Her(ϕ) can be solved in polynomial time whenever the quantifier prefix of ϕ is Q. Otherwise, Q contains ∃∃∀ or ∃∀∃ as a subword, and in this case, there is a first-order formula ϕ whose quantifier prefix is Q and Her(ϕ) is coNP-complete. Moreover, we show that there is no algorithm that decides for a given first-order formula ϕ whether Her(ϕ) is in P (unless P=NP).
Cite as
Manuel Bodirsky and Santiago Guzmán-Pro. Hereditary First-Order Logic: the Tractable Quantifier Prefix Classes. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 6:1-6:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{bodirsky_et_al:LIPIcs.CSL.2026.6,
author = {Bodirsky, Manuel and Guzm\'{a}n-Pro, Santiago},
title = {{Hereditary First-Order Logic: the Tractable Quantifier Prefix Classes}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {6:1--6:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.6},
URN = {urn:nbn:de:0030-drops-254308},
doi = {10.4230/LIPIcs.CSL.2026.6},
annote = {Keywords: Quantifier prefix, first-order Logic, Computational Complexity, Polynomial-time algorithm, coNP-completeness}
}
Document
Bridging Weighted First Order Model Counting and Graph Polynomials
Abstract
The Weighted First-Order Model Counting Problem (WFOMC) asks to compute the weighted sum of models of a given first-order logic sentence over a given domain. It can be solved in time polynomial in the domain size for sentences from the two-variable fragment with counting quantifiers, known as C^2. This polynomial-time complexity is known to be retained when extending C^2 by one of the following axioms: linear order axiom, tree axiom, forest axiom, directed acyclic graph axiom or connectedness axiom. An interesting question remains as to which other axioms can be added to the first-order sentences in this way. We provide a new perspective on this problem by associating WFOMC with graph polynomials. Using WFOMC, we define Weak Connectedness Polynomial and Strong Connectedness Polynomials for first-order logic sentences. It turns out that these polynomials have the following interesting properties. First, they can be computed in polynomial time in the domain size for sentences from C^2. Second, we can use them to solve WFOMC with all of the existing axioms known to be tractable as well as with new ones such as bipartiteness, strong connectedness, having k connected components, etc. Third, the well-known Tutte polynomial can be recovered as a special case of the Weak Connectedness Polynomial, and the Strict and Non-Strict Directed Chromatic Polynomials can be recovered from the Strong Connectedness Polynomials.
Cite as
Qipeng Kuang, Ondřej Kuželka, Yuanhong Wang, and Yuyi Wang. Bridging Weighted First Order Model Counting and Graph Polynomials. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 7:1-7:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{kuang_et_al:LIPIcs.CSL.2026.7,
author = {Kuang, Qipeng and Ku\v{z}elka, Ond\v{r}ej and Wang, Yuanhong and Wang, Yuyi},
title = {{Bridging Weighted First Order Model Counting and Graph Polynomials}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {7:1--7:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.7},
URN = {urn:nbn:de:0030-drops-254316},
doi = {10.4230/LIPIcs.CSL.2026.7},
annote = {Keywords: Weighted First-Order Model Counting, Axiom, Enumerative Combinatorics, Tutte Polynomial}
}
Document
Register-Bounded Synthesis from Constraint LTL
Abstract
We consider synthesis problems from logical specifications over infinite data domains, expressed in the logic constraint LTL (CLTL), which extends LTL with predicates over an infinite set of data values. We consider register-bounded synthesis, where the goal is to automatically generate, if it exists, a transducer with r registers that realizes a given CLTL formula, where r is also given as input. We prove that CLTL register-bounded synthesis is 2ExpTime-c for various data domains such as any infinite set with equality, (ℚ, <), and (ℕ, <). For the latter domain, this contrasts with known undecidability results of (unbounded) register CLTL synthesis, by Bhaskar and Praveen. Lastly, we consider synthesis in a partial observation setting by extending CLTL with invisible variables.
Cite as
Nino Dauvier, Emmanuel Filiot, and Pierre-Alain Reynier. Register-Bounded Synthesis from Constraint LTL. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{dauvier_et_al:LIPIcs.CSL.2026.8,
author = {Dauvier, Nino and Filiot, Emmanuel and Reynier, Pierre-Alain},
title = {{Register-Bounded Synthesis from Constraint LTL}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {8:1--8:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.8},
URN = {urn:nbn:de:0030-drops-254322},
doi = {10.4230/LIPIcs.CSL.2026.8},
annote = {Keywords: Synthesis, Data words, Constraint linear time logic, Register transducer}
}
Document
Arity Hierarchies for Quantifiers Closed Under Partial Polymorphisms
Abstract
We investigate the expressive power of generalized quantifiers closed under partial polymorphism conditions motivated by the study of constraint satisfaction problems. We answer a number of questions arising from the work of Dawar and Hella (CSL 2024) where such quantifiers were introduced. For quantifiers closed under partial near-unanimity polymorphisms, we establish hierarchy results clarifying the interplay between the arity of the polymorphisms and of the quantifiers: The expressive power of (𝓁+1)-ary quantifiers closed under 𝓁-ary partial near-unanimity polymorphisms is strictly between the class of all quantifiers of arity 𝓁-1 and 𝓁. We also establish an infinite hierarchy based on the arity of quantifiers with a fixed arity of partial near-unanimity polymorphisms. Finally, we prove inexpressiveness results for quantifiers with a partial Maltsev polymorphism. The separation results are proved using novel algebraic constructions in the style of Cai-Fürer-Immerman and the quantifier pebble games of Dawar and Hella (2024).
Cite as
Anuj Dawar, Lauri Hella, and Benedikt Pago. Arity Hierarchies for Quantifiers Closed Under Partial Polymorphisms. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 9:1-9:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{dawar_et_al:LIPIcs.CSL.2026.9,
author = {Dawar, Anuj and Hella, Lauri and Pago, Benedikt},
title = {{Arity Hierarchies for Quantifiers Closed Under Partial Polymorphisms}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {9:1--9:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.9},
URN = {urn:nbn:de:0030-drops-254330},
doi = {10.4230/LIPIcs.CSL.2026.9},
annote = {Keywords: finite model theory, constraint satisfaction problems, generalized quantifiers}
}
Document
Disjunctions of Two Dependence Atoms
Abstract
Dependence logic is a formalism that augments the syntax of first-order logic with dependence atoms asserting that the value of a variable is determined by the values of some other variables, i.e., dependence atoms express functional dependencies in relational databases. On finite structures, dependence logic captures NP, hence there are sentences of dependence logic whose model-checking problem is NP-complete. In fact, it is known that there are disjunctions of three dependence atoms whose model-checking problem is NP-complete. Motivated from considerations in database theory, we study the model-checking problem for disjunctions of two unary dependence atoms and establish a trichotomy theorem, namely, for every such formula, one of the following is true for the model-checking problem: (i) it is NL-complete; (ii) it is L-complete; (iii) it is first-order definable (hence, in AC⁰). Furthermore, we classify the complexity of the model-checking problem for disjunctions of two arbitrary dependence atoms, and also characterize when such a disjunction is coherent, i.e., when it satisfies a certain small-model property. Along the way, we identify a new class of 2CNF-formulas whose satisfiability problem is L-complete.
Cite as
Nicolas Fröhlich, Phokion G. Kolaitis, and Arne Meier. Disjunctions of Two Dependence Atoms. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 10:1-10:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{frohlich_et_al:LIPIcs.CSL.2026.10,
author = {Fr\"{o}hlich, Nicolas and Kolaitis, Phokion G. and Meier, Arne},
title = {{Disjunctions of Two Dependence Atoms}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {10:1--10:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.10},
URN = {urn:nbn:de:0030-drops-254343},
doi = {10.4230/LIPIcs.CSL.2026.10},
annote = {Keywords: Dependence logic, coherence, model-checking, complexity, functional dependencies}
}
Document
A Complete Diagrammatic Calculus for Conditional Gaussian Mixtures
Abstract
We extend the synthetic theories of discrete and Gaussian categorical probability by introducing a diagrammatic calculus for reasoning about hybrid probabilistic models in which continuous random variables, conditioned on discrete ones, follow a multivariate Gaussian distribution. This setting includes important families of distributions such as Gaussian mixtures, where each Gaussian component is selected according to a discrete variable. We develop a string diagrammatic syntax for distributions of this type, give it a compositional semantics, and equip it with a sound and complete equational theory that characterises when two mixtures represent the same distribution.
Cite as
Mateo Torres-Ruiz, Robin Piedeleu, Alexandra Silva, and Fabio Zanasi. A Complete Diagrammatic Calculus for Conditional Gaussian Mixtures. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 11:1-11:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{torresruiz_et_al:LIPIcs.CSL.2026.11,
author = {Torres-Ruiz, Mateo and Piedeleu, Robin and Silva, Alexandra and Zanasi, Fabio},
title = {{A Complete Diagrammatic Calculus for Conditional Gaussian Mixtures}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {11:1--11:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.11},
URN = {urn:nbn:de:0030-drops-254358},
doi = {10.4230/LIPIcs.CSL.2026.11},
annote = {Keywords: String diagrams, Category theory, Mixture models, Probability theory}
}
Document
String Diagrams for Closed Symmetric Monoidal Categories
Abstract
We introduce a graphical language for closed symmetric monoidal categories based on an extension of string diagrams with special bracket wires representing internal homs. These bracket wires make the structure of the internal hom functor explicit, allowing standard morphism wires to interact with them through a well-defined set of graphical rules. We establish the soundness and completeness of the diagrammatic calculus, and illustrate its expressiveness through examples drawn from category theory, logic and programming language semantics.
Cite as
Callum Reader and Alessandro Di Giorgio. String Diagrams for Closed Symmetric Monoidal Categories. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 12:1-12:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{reader_et_al:LIPIcs.CSL.2026.12,
author = {Reader, Callum and Di Giorgio, Alessandro},
title = {{String Diagrams for Closed Symmetric Monoidal Categories}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {12:1--12:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.12},
URN = {urn:nbn:de:0030-drops-254369},
doi = {10.4230/LIPIcs.CSL.2026.12},
annote = {Keywords: diagrammatic languages, logic, lambda calculi}
}
Document
Compactness in Semiring Semantics
Abstract
Semiring provenance was originally introduced in database theory with the aim of explaining why certain tuples are (not) contained in the answer of a query. To this end, logical statements are not just evaluated to true or false but to values in a commutative semiring. Depending on the underlying semiring, this allows us to track descriptions of the atomic facts that are responsible for the truth of a statement or practical information about the evaluation such as costs or confidence. Recently, this approach has been expanded to a systematic study of semiring semantics for first-order logic and other logical systems. This raises the question to what extent model-theoretic results can be generalised to semiring semantics and how this relates to the algebraic properties of the underlying semiring.
Here we investigate the availability of compactness in semiring semantics. The appropriate setting for this is based on absorptive semirings with well-defined infinitary products. Compactness can be stated either in terms of satisfiability or in terms of entailment, and these two variants are trivially equivalent in Boolean semantics. However, this is no longer the case in semiring semantics. Compactness in terms of satisfiability, defined as the existence of non-zero valuations, indeed generalises to every infinitary absorptive semiring. For compactness in terms of entailment the situation is different. The entailment relation naturally extends to semiring semantics (via the natural order on the semiring) but this yields a stronger variant of compactness, which fails for certain important semirings, including the tropical semiring and the Łukasiewicz semiring. Our main positive results show that strong compactness does indeed hold for all finite semirings and all lattice semirings.
Cite as
Sophie Brinke, Anuj Dawar, Erich Grädel, Lovro Mrkonjić, and Matthias Naaf. Compactness in Semiring Semantics. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 13:1-13:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{brinke_et_al:LIPIcs.CSL.2026.13,
author = {Brinke, Sophie and Dawar, Anuj and Gr\"{a}del, Erich and Mrkonji\'{c}, Lovro and Naaf, Matthias},
title = {{Compactness in Semiring Semantics}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {13:1--13:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.13},
URN = {urn:nbn:de:0030-drops-254372},
doi = {10.4230/LIPIcs.CSL.2026.13},
annote = {Keywords: Semiring semantics, compactness}
}
Document
Satisfiability in Łukasiewicz Logic and Its Unbounded Relative
Abstract
Unbounded Łukasiewicz logic is a substructural logic that combines features of infinite-valued Łukasiewicz logic with those of abelian logic. The logic is finitely strongly complete w.r.t. the additive 𝓁-group on the reals expanded with a distinguished element -1. We show that the existential theory of this structure is NP-complete. This provides a complexity upper bound for the set of theorems and the finite consequence relation of unbounded Łukasiewicz logic. The result is obtained by reducing the problem to the existential theory of the MV-algebra on the reals, the standard semantics of Łukasiewicz logic. This provides a new connection between both logics. The result entails a translation of the existential theory of the standard MV-algebra into itself.
Cite as
Zuzana Haniková and Filip Jankovec. Satisfiability in Łukasiewicz Logic and Its Unbounded Relative. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{hanikova_et_al:LIPIcs.CSL.2026.14,
author = {Hanikov\'{a}, Zuzana and Jankovec, Filip},
title = {{Satisfiability in {\L}ukasiewicz Logic and Its Unbounded Relative}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {14:1--14:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.14},
URN = {urn:nbn:de:0030-drops-254380},
doi = {10.4230/LIPIcs.CSL.2026.14},
annote = {Keywords: unbounded {\L}ukasiewicz Logic, {\L}ukasiewicz Logic, Abelian Logic, existential theory, computational complexity, NP-completeness}
}
Document
Cyclic Proof Theory of Generalised Inductive Definitions
Abstract
We study cyclic proof systems for μPA, an extension of Peano arithmetic by generalised inductive definitions that is arithmetically equivalent to the (impredicative) subsystem of second-order arithmetic Π^1_2-CA₀ by Möllerfeld.
The main result of this paper is that cyclic and inductive μPA have the same proof-theoretic strength. First, we translate cyclic proofs into an annotated variant based on Sprenger and Dam’s systems for first-order μ-calculus, whose stronger validity condition allows for a simpler proof of soundness. We then formalise this argument within Π^1_2-CA₀, leveraging Möllerfeld’s conservativity properties. To this end, we build on prior work by Curzi and Das on the reverse mathematics of the Knaster-Tarski theorem.
As a byproduct of our proof methods we show that, despite the stronger validity condition, annotated and "plain" cyclic proofs for μPA prove the same theorems.
This work represents a further step in the non-wellfounded proof-theoretic analysis of theories of arithmetic via impredicative fragments of second-order arithmetic, an approach initiated by Simpson’s Cyclic Arithmetic, and continued by Das and Melgaard in the context of arithmetical inductive definitions.
Cite as
Gianluca Curzi and Lukas Melgaard. Cyclic Proof Theory of Generalised Inductive Definitions. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 15:1-15:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{curzi_et_al:LIPIcs.CSL.2026.15,
author = {Curzi, Gianluca and Melgaard, Lukas},
title = {{Cyclic Proof Theory of Generalised Inductive Definitions}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {15:1--15:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.15},
URN = {urn:nbn:de:0030-drops-254399},
doi = {10.4230/LIPIcs.CSL.2026.15},
annote = {Keywords: cyclic proofs, positive inductive definitions, arithmetic, fixed points, proof theory, reset proof systems}
}
Document
On the Entailment Problem in Dynamic Separation Logic with Inductive Definitions
Abstract
Separation Logic (SL) is a well-established framework for reasoning about programs that manipulate dynamic memory. To express and verify properties of custom recursive data structures, SL is extended with spatial predicates defined by user-specified inductive rules. Many verification problems reduce to deciding entailments between formulas involving these predicates. While the general entailment problem is undecidable, a broad class of inductive rules - known as PCE (Progressing, Connected, and Established) - has been identified for which entailment is decidable. In this work, we extend the study of the entailment problem to Dynamic Separation Logic (DSL), an extension of SL that includes dynamic modalities for reasoning about actions on the heap and store. We show that entailment in DSL remains decidable for PCE rules by proving that dynamic modalities can be automatically eliminated.
Cite as
Nicolas Peltier. On the Entailment Problem in Dynamic Separation Logic with Inductive Definitions. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 16:1-16:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{peltier:LIPIcs.CSL.2026.16,
author = {Peltier, Nicolas},
title = {{On the Entailment Problem in Dynamic Separation Logic with Inductive Definitions}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {16:1--16:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.16},
URN = {urn:nbn:de:0030-drops-254402},
doi = {10.4230/LIPIcs.CSL.2026.16},
annote = {Keywords: Separation logic, Dynamic logic, Entailment problem}
}
Document
A Uniform Cut-Elimination Theorem for Linear Logics with Fixed Points and Super Exponentials
Abstract
In the realm of light logics deriving from linear logic, a number of variants of exponential rules have been investigated. The profusion of such proof systems induces the need for cut-elimination theorems for each logic, the proofs of which may be redundant. A number of approaches in proof theory have been adopted to cope with this need. In the present paper, we consider this issue from the point of view of enhancing linear logic with least and greatest fixed-points and considering such a variety of exponential connectives.
Our main contribution is to provide a uniform cut-elimination theorem for a parametrized system with fixed-points by combining two approaches: cut-elimination proofs by reduction (or translation) to another system and the identification of sufficient conditions for cut-elimination.
More precisely, we examine a broad range of systems, taking inspiration from Nigam and Miller’s subexponentials and from the first author and Laurent’s super exponentials. Our work is motivated, on the one hand, by Baillot’s work on light logics with recursive types and on the other hand by our recent work on the proof theory of the modal μ-calculus.
Cite as
Alexis Saurin and Esaïe Bauer. A Uniform Cut-Elimination Theorem for Linear Logics with Fixed Points and Super Exponentials. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 17:1-17:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{saurin_et_al:LIPIcs.CSL.2026.17,
author = {Saurin, Alexis and Bauer, Esa\"{i}e},
title = {{A Uniform Cut-Elimination Theorem for Linear Logics with Fixed Points and Super Exponentials}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {17:1--17:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.17},
URN = {urn:nbn:de:0030-drops-254418},
doi = {10.4230/LIPIcs.CSL.2026.17},
annote = {Keywords: cut elimination, exponential modalities, fixed-points, linear logic, light logics, mu-calculus, non-wellfounded proofs, proof theory, sequent calculus, subexponentials, super exponentials}
}
Document
A Modular Framework for Proof-Search via Formalised Modal Completeness in HOL Light
Abstract
We extend the existing HOL Light Library for Modal Systems (HOLMS) to support a modular implementation of modal reasoning within the HOL Light proof assistant. We deeply embed axiomatic calculi and relational semantics for seven normal modal logics (K, T, B, K4, S4, S5, GL) and formalise modal adequacy theorems for these systems. We then leverage those formalisations to implement a mechanism for automated reasoning via proof-search in the associated labelled sequent calculi, which we shallowly embed in HOL Light’s goal-stack mechanism. This way, we equip the general-purpose proof assistant with (semi)decision procedures for these logics that, in case of failure to construct a proof for the input formula, return a certified countermodel within the appropriate class for the logic under consideration. On the methodological side, we propose a precise measure of the modularity of our approach by systematically adopting Christopher Strachey’s distinction between ad hoc and parametric polymorphism throughout the library.
Cite as
Antonella Bilotta, Marco Maggesi, and Cosimo Perini Brogi. A Modular Framework for Proof-Search via Formalised Modal Completeness in HOL Light. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 18:1-18:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{bilotta_et_al:LIPIcs.CSL.2026.18,
author = {Bilotta, Antonella and Maggesi, Marco and Perini Brogi, Cosimo},
title = {{A Modular Framework for Proof-Search via Formalised Modal Completeness in HOL Light}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {18:1--18:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.18},
URN = {urn:nbn:de:0030-drops-254427},
doi = {10.4230/LIPIcs.CSL.2026.18},
annote = {Keywords: Modal logic, HOL Light, Labelled sequent calculi, Logical verification, Interactive theorem proving, Automated proof-search}
}
Document
A Unifying Conservation Theorem
Abstract
The relationship between classical and constructive logics has long been illuminated by a series of conservation results, beginning with Kolmogorov’s negative translation and Glivenko’s double negation theorem, and later extended by Kuroda and Segerberg to first-order and minimal logics respectively. These results reveal how certain classical principles can be interpreted or recovered within weaker constructive frameworks, either via translations or through minimal extensions that satisfy specific logical properties. In this paper, we propose a unifying generalisation of these conservation theorems, that consolidates and expands the abstract methods introduced in earlier studies, offering a unified perspective on the interplay between classical provability and constructive reasoning.
Cite as
Giulio Fellin. A Unifying Conservation Theorem. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 19:1-19:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{fellin:LIPIcs.CSL.2026.19,
author = {Fellin, Giulio},
title = {{A Unifying Conservation Theorem}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {19:1--19:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.19},
URN = {urn:nbn:de:0030-drops-254431},
doi = {10.4230/LIPIcs.CSL.2026.19},
annote = {Keywords: double negation, negative translation, conservation, minimal logic, Glivenko’s theorem}
}
Document
On Left Adjoints Preserving Colimits in HoTT
Abstract
We examine how the standard proof that left adjoints preserve colimits behaves in the setting of wild categories, a natural setting for synthetic homotopy theory inside homotopy type theory. We prove that the proof may fail for adjunctions between wild categories. Our core contribution, however, is a sufficient condition on the left adjoint for the proof to go through. The condition, called 2-coherence, expresses that the naturality structure of the hom-isomorphism commutes with composition of morphisms. We present two useful examples of this condition in action. First, we use it, along with a new version of a known trick for homogeneous types, to show that the suspension functor preserves graph-indexed colimits. Second, we show that every modality, viewed as a functor on coslices of a type universe, is 2-coherent as a left adjoint to the forgetful functor from the subcategory of modal types, thereby proving this subcategory is cocomplete. We have formalized our main results in Agda.
Cite as
Perry Hart. On Left Adjoints Preserving Colimits in HoTT. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 20:1-20:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{hart:LIPIcs.CSL.2026.20,
author = {Hart, Perry},
title = {{On Left Adjoints Preserving Colimits in HoTT}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {20:1--20:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.20},
URN = {urn:nbn:de:0030-drops-254442},
doi = {10.4230/LIPIcs.CSL.2026.20},
annote = {Keywords: wild categories, colimits, adjunctions, homotopy type theory, category theory, synthetic homotopy theory, higher inductive types, modalities}
}
Document
Classifying Covering Types in Homotopy Type Theory
Abstract
Covering spaces are a fundamental tool in algebraic topology because of the close relationship they bear with the fundamental groups of spaces. Indeed, they are in correspondence with the subgroups of the fundamental group: this is known as the Galois correspondence. In particular, the covering space corresponding to the trivial group is the universal covering, which is a "1-connected" variant of the original space, in the sense that it has the same homotopy groups, except for the first one which is trivial. In this article, we formalize this correspondence in homotopy type theory, a variant of Martin-Löf type theory in which types can be interpreted as spaces (up to homotopy). Along the way, we develop an n-dimensional generalization of covering spaces. Moreover, in order to demonstrate the applicability of our approach, we formally classify the covering of lens spaces and explain how to construct the Poincaré homology sphere.
Cite as
Samuel Mimram and Émile Oleon. Classifying Covering Types in Homotopy Type Theory. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 21:1-21:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{mimram_et_al:LIPIcs.CSL.2026.21,
author = {Mimram, Samuel and Oleon, \'{E}mile},
title = {{Classifying Covering Types in Homotopy Type Theory}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {21:1--21:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.21},
URN = {urn:nbn:de:0030-drops-254456},
doi = {10.4230/LIPIcs.CSL.2026.21},
annote = {Keywords: homotopy type theory, covering, Galois correspondence}
}
Document
On the Algorithmic Structure of Dialectica Realisers
Abstract
Gödel’s Dialectica interpretation is a fundamental tool for the extraction of computational content from proofs, and plays a central role in today’s proof mining program. In the past decades, it has also been studied from the perspective of programming languages, and our contribution is in that direction. Specifically, we present Dialectica as a collection of rules in the style of Hoare logic, where Dialectica is now viewed as a language for specifying procedural programs that come with a forward and backward direction. This viewpoint captures the interesting dynamics of realisers extracted by the Dialectica interpretation, and we illustrate this by defining a generalised backpropagation semantics for a fragment of this language. We envisage this work as providing a base for several future developments, both theoretical and practical, which we outline at the end.
Cite as
Davide Barbarossa and Thomas Powell. On the Algorithmic Structure of Dialectica Realisers. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 22:1-22:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{barbarossa_et_al:LIPIcs.CSL.2026.22,
author = {Barbarossa, Davide and Powell, Thomas},
title = {{On the Algorithmic Structure of Dialectica Realisers}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {22:1--22:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.22},
URN = {urn:nbn:de:0030-drops-254466},
doi = {10.4230/LIPIcs.CSL.2026.22},
annote = {Keywords: Dialectica interpretation, Hoare logic, Programs from proofs}
}
Document
A Logic for Fresh Labelled Transition Systems
Abstract
We introduce a Hennessy-Milner logic with recursion for Fresh Labelled Transition Systems (FLTSs). These are nominal labelled transition systems which keep track of the history, i.e. of data values seen so far, and can model fresh data generation. In particular, FLTSs generalise the computations of Fresh-Register Automata, which in turn can be seen as a "regular" class of history-tracking automata operating on infinite input alphabets. The logic we introduce is a modal mu-calculus equipped with infinite disjunctions over arbitrary and fresh data values respectively, while its recursion is parameterised on vectors of data values. It can express a variety of properties, such as the existence of an infinite path of distinct data values, the absence of paths where values are repeated, or the existence of a finite path where some taint property is violated. We study the model-checking problem and its complexity via a reduction to parity games and, using nominal sets techniques, provide an exponential upper bound for it.
Cite as
Mohamed H. Bandukara and Nikos Tzevelekos. A Logic for Fresh Labelled Transition Systems. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 23:1-23:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{bandukara_et_al:LIPIcs.CSL.2026.23,
author = {Bandukara, Mohamed H. and Tzevelekos, Nikos},
title = {{A Logic for Fresh Labelled Transition Systems}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {23:1--23:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.23},
URN = {urn:nbn:de:0030-drops-254478},
doi = {10.4230/LIPIcs.CSL.2026.23},
annote = {Keywords: Nominal Transition Systems, Hennessy-Milner Logic, Modal Mu-Calculus, Register Automata, Nominal Sets, Parity Games}
}
Document
Well-Founded Coalgebras Meet Kőnig’s Lemma
Abstract
Kőnig’s lemma is a fundamental result about trees with countless applications in mathematics and computer science. In contrapositive form, it states that if a tree is finitely branching and well-founded (i.e. has no infinite paths), then it is finite. We present a coalgebraic version of Kőnig’s lemma featuring two dimensions of generalization: from finitely branching trees to coalgebras for a finitary endofunctor H, and from the base category of sets to a locally finitely presentable category ℂ, such as the category of posets, nominal sets, or convex sets. Our coalgebraic Kőnig’s lemma states that, under mild assumptions on ℂ and H, every well-founded coalgebra for H is the directed join of its well-founded subcoalgebras with finitely generated state space - in particular, the category of well-founded coalgebras is locally presentable. As applications, we derive versions of Kőnig’s lemma for graphs in a topos as well as for nominal and convex transition systems. Additionally, we show that the key construction underlying the proof gives rise to two simple constructions of the initial algebra (equivalently, the final recursive coalgebra) for the functor H: The initial algebra is both the colimit of all well-founded and of all recursive coalgebras with finitely presentable state space. Remarkably, this result holds even in settings where well-founded coalgebras form a proper subclass of recursive ones. The first construction of the initial algebra is entirely new, while for the second one our approach yields a short and transparent new correctness proof.
Cite as
Henning Urbat and Thorsten Wißmann. Well-Founded Coalgebras Meet Kőnig’s Lemma. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{urbat_et_al:LIPIcs.CSL.2026.24,
author = {Urbat, Henning and Wi{\ss}mann, Thorsten},
title = {{Well-Founded Coalgebras Meet K\H{o}nig’s Lemma}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {24:1--24:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.24},
URN = {urn:nbn:de:0030-drops-254485},
doi = {10.4230/LIPIcs.CSL.2026.24},
annote = {Keywords: K\H{o}nig’s Lemma, Well-Foundedness, Coalgebra}
}
Document
Constructing Witnesses for Lower Bounds on Behavioural Distances
Abstract
Behavioural distances provide a robust alternative to notions of equivalence such as bisimilarity in the context of probabilistic transition systems. They can be defined as least fixed points, whose universal property allows us to exhibit upper bounds on the distance between states, showing them to be at most some distance apart.
In this paper, we instead consider the problem of bounding distances from below, showing states to be at least some distance apart. Contrary to upper bounds, it is possible to reason about lower bounds inductively. We exploit this by giving an inductive derivation system for lower bounds on an existing definition of behavioural distance for labelled Markov chains. This is inspired by recent work on apartness as an inductive counterpart to bisimilarity. Proofs in our system will be shown to closely match the behavioural distance by soundness and (approximate) completeness results.
We further provide a constructive correspondence between our derivation system and formulas in a modal logic with quantitative semantics. This logic was used in recent work of Rady and van Breugel to construct evidence for lower bounds on behavioural distances. Our constructions provide smaller witnessing formulas in many examples.
Cite as
Ruben Turkenburg, Harsh Beohar, Franck van Breugel, Clemens Kupke, and Jurriaan Rot. Constructing Witnesses for Lower Bounds on Behavioural Distances. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 25:1-25:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{turkenburg_et_al:LIPIcs.CSL.2026.25,
author = {Turkenburg, Ruben and Beohar, Harsh and van Breugel, Franck and Kupke, Clemens and Rot, Jurriaan},
title = {{Constructing Witnesses for Lower Bounds on Behavioural Distances}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {25:1--25:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.25},
URN = {urn:nbn:de:0030-drops-254493},
doi = {10.4230/LIPIcs.CSL.2026.25},
annote = {Keywords: Behavioural Distances, Markov Chains, Apartness}
}
Document
ε-Distance via Lévy-Prokhorov Lifting
Abstract
The most studied and accepted pseudometric for probabilistic processes is one based on the Kantorovich distance between distributions. It comes with many theoretical and motivating results, in particular it is the fixpoint of a given functional and defines a functor on (complete) pseudometric spaces. It is also the foundation for a categorical lifting of pseudometrics.
Other notions of behavioural pseudometrics have also been proposed, one of them (ε-distance) based on ε-bisimulation. ε-Distance has the advantages that it is intuitively easy to understand, it relates systems that are conceptually close (for example, an imperfect implementation is close to its specification), and it comes equipped with a natural notion of ε-coupling. Finally, this distance is easy to compute.
We show that ε-distance is also the greatest fixpoint of a functional and provides a functor. The latter is obtained by replacing the Kantorovich distance in the lifting functor with the Lévy-Prokhorov distance. In addition, we show that ε-couplings and ε-bisimulations have an appealing coalgebraic characterization.
Cite as
Josée Desharnais and Ana Sokolova. ε-Distance via Lévy-Prokhorov Lifting. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 26:1-26:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{desharnais_et_al:LIPIcs.CSL.2026.26,
author = {Desharnais, Jos\'{e}e and Sokolova, Ana},
title = {{\epsilon-Distance via L\'{e}vy-Prokhorov Lifting}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {26:1--26:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.26},
URN = {urn:nbn:de:0030-drops-254506},
doi = {10.4230/LIPIcs.CSL.2026.26},
annote = {Keywords: L\'{e}vy-Prokhorov metric, behavioural distance, epsilon-bisimulation, reactive probabilistic transition systems, discrete labelled Markov processes, coalgebraic epsilon-(bi)simulation}
}
Document
Analysis of Logics with Arithmetic
Abstract
We present new results on finite satisfiability of logics with counting and arithmetic. One result is a tight bound on the complexity of satisfiability of logics with so-called local Presburger quantifiers, which sum over neighbors of a node in a graph. A second contribution concerns computing a semilinear representation of the cardinalities associated with a formula in two variable logic extended with counting quantifiers. Such a representation allows you to get bounds not only on satisfiability for these logics, but for satisfiability in the presence of additional "global cardinality constraints": restrictions on cardinalities of unary formulas, expressed using arbitrary decidability logics over arithmetic. In the process, we provide simpler proofs of some key prior results on finite satisfiability and semi-linearity of the spectrum for these logics.
Cite as
Michael Benedikt, Chia-Hsuan Lu, and Tony Tan. Analysis of Logics with Arithmetic. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 27:1-27:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{benedikt_et_al:LIPIcs.CSL.2026.27,
author = {Benedikt, Michael and Lu, Chia-Hsuan and Tan, Tony},
title = {{Analysis of Logics with Arithmetic}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {27:1--27:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.27},
URN = {urn:nbn:de:0030-drops-254510},
doi = {10.4230/LIPIcs.CSL.2026.27},
annote = {Keywords: Presburger quantifiers, Spectrum, Guarded logics}
}
Document
Resourceful Traces for Commuting Processes
Abstract
We show that, when the actions of a Mazurkiewicz trace are considered not merely as atomic but as transformations from a specified type of inputs to a specified type of outputs, we obtain a novel notion of presentation for effectful categories (also known as generalized Freyd categories), a well-known algebraic structure in the semantics of side-effecting computation. Like the usual representation of traces as graphs, our notion of presentation gives rise to a graphical representation of morphisms in effectful categories. We use our presentations to give a construction of the commuting tensor product of free effectful categories, capturing the combination of systems in which the actions of each must commute with one another, while still permitting exchange of resources.
Cite as
Matthew Earnshaw, Chad Nester, and Mario Román. Resourceful Traces for Commuting Processes. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 28:1-28:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{earnshaw_et_al:LIPIcs.CSL.2026.28,
author = {Earnshaw, Matthew and Nester, Chad and Rom\'{a}n, Mario},
title = {{Resourceful Traces for Commuting Processes}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {28:1--28:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.28},
URN = {urn:nbn:de:0030-drops-254522},
doi = {10.4230/LIPIcs.CSL.2026.28},
annote = {Keywords: Mazurkiewicz traces, premonoidal categories, monoidal categories, effectful categories}
}
Document
Parametric Iteration in Resource Theories
Abstract
Many algorithms are specified with respect to a fixed but unknown parameter. Examples of this are especially common in cryptography, where protocols often feature a security parameter such as the bit length of a secret key.
Our aim is to capture this phenomenon in a more abstract setting. We focus on resource theories - general calculi of processes with a string diagrammatic syntax - introducing a general parametric iteration construction. By instantiating this construction within the Markov category of probabilistic Boolean circuits and equipping it with a suitable metric, we are able to capture the notion of negligibility via asymptotic equivalence, in a compositional way. This allows us to use diagrammatic reasoning to prove simple cryptographic theorems - for instance, proving that guessing a randomly generated key has negligible success.
Cite as
Alessandro Di Giorgio, Pawel Sobocinski, and Niels Voorneveld. Parametric Iteration in Resource Theories. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 29:1-29:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{digiorgio_et_al:LIPIcs.CSL.2026.29,
author = {Di Giorgio, Alessandro and Sobocinski, Pawel and Voorneveld, Niels},
title = {{Parametric Iteration in Resource Theories}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {29:1--29:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.29},
URN = {urn:nbn:de:0030-drops-254541},
doi = {10.4230/LIPIcs.CSL.2026.29},
annote = {Keywords: Markov categories, Cryptography, String diagrams, Asymptotic equivalence}
}
Document
Reward Interfaces with Best-Effort Implementations
Abstract
Interface theories, notably interface automata, serve as expressive frameworks for component-based design, specifying component behavior and interaction in concurrent systems. Traditional interface formalisms specify assumptions that a component’s environment must satisfy and the guarantees that each component provides. This qualitative view of component interaction based on imposing strict assumptions and Boolean guarantees may, however, not be expressive enough to capture the system’s allowed or desired behaviors under different environments.
In this paper, we introduce reward interfaces to support component-based design while accommodating multi-valued correctness requirements and adaptive best-effort satisfaction of component’s guarantees. Building upon interface automata, our framework enables modeling a rich class of quantitative component specifications. We propose formal notions of implementation, refinement and compatibility for reward interfaces. We study a class of reward interfaces with automata-based representations, for which we provide algorithms for checking compatibility and refinement, and existence of best-effort implementations. Our framework offers a comprehensive approach to reward interface specification and design.
Cite as
Rafael Dewes and Rayna Dimitrova. Reward Interfaces with Best-Effort Implementations. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 30:1-30:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{dewes_et_al:LIPIcs.CSL.2026.30,
author = {Dewes, Rafael and Dimitrova, Rayna},
title = {{Reward Interfaces with Best-Effort Implementations}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {30:1--30:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.30},
URN = {urn:nbn:de:0030-drops-254553},
doi = {10.4230/LIPIcs.CSL.2026.30},
annote = {Keywords: Component-based design, interface automata, quantitative specifications}
}
Document
Parametric Disjunctive Timed Networks
Abstract
We consider distributed systems with an arbitrary number of processes, modelled by timed automata that communicate through location guards: a process can take a guarded transition if at least one other process is in a given location. In this work, we introduce parametric disjunctive timed networks, where each timed automaton may contain timing parameters, i.e., unknown constants. We investigate two problems: deciding the emptiness of the set of parameter valuations for which 1) a given location is reachable for at least one process (local property), and 2) a global state is reachable where all processes are in a given location (global property). Our main positive result is that the first problem is decidable for networks of processes with a single clock and without invariants; this result holds for arbitrarily many timing parameters - a setting with few known decidability results. However, it becomes undecidable when invariants are allowed, or when considering global properties, even for systems with a single parameter. This highlights the significant expressive power of invariants in these networks. Additionally, we exhibit further decidable subclasses by restraining the syntax of guards and invariants.
Cite as
Étienne André, Swen Jacobs, and Engel Lefaucheux. Parametric Disjunctive Timed Networks. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 31:1-31:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{andre_et_al:LIPIcs.CSL.2026.31,
author = {Andr\'{e}, \'{E}tienne and Jacobs, Swen and Lefaucheux, Engel},
title = {{Parametric Disjunctive Timed Networks}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {31:1--31:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.31},
URN = {urn:nbn:de:0030-drops-254562},
doi = {10.4230/LIPIcs.CSL.2026.31},
annote = {Keywords: parametrised verification, parametric timed automata, verification of infinite-state systems}
}
Document
Mean-Payoff and Energy Discrete-Bidding Games
Abstract
A bidding game is played on a graph as follows. A token is placed on an initial vertex and both players are allocated budgets. In each turn, the players simultaneously submit bids that do not exceed their available budgets, the higher bidder moves the token, and pays the bid to the lower bidder. We focus on discrete-bidding, which are motivated by practical applications and restrict the granularity of the players' bids, e.g, bids must be given in cents. We study, for the first time, discrete-bidding games with mean-payoff and energy objectives. In contrast, mean-payoff continuous-bidding games (i.e., no granularity restrictions) are understood and exhibit a rich mathematical structure. The threshold budget is a necessary and sufficient initial budget for winning an energy game or guaranteeing a target payoff in a mean-payoff game. We first establish existence of threshold budgets; a non-trivial property due to the concurrent moves of the players. Moreover, we identify the structure of the thresholds, which is key in obtaining compact strategies, and in turn, showing that finding threshold is in NP and coNP even in succinctly-represented games.
Cite as
Guy Avni and Suman Sadhukhan. Mean-Payoff and Energy Discrete-Bidding Games. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 32:1-32:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{avni_et_al:LIPIcs.CSL.2026.32,
author = {Avni, Guy and Sadhukhan, Suman},
title = {{Mean-Payoff and Energy Discrete-Bidding Games}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {32:1--32:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.32},
URN = {urn:nbn:de:0030-drops-254573},
doi = {10.4230/LIPIcs.CSL.2026.32},
annote = {Keywords: Bidding games, Discrete-bidding, Mean-payoff games, energy games}
}
Document
Deciding the Value of Two-Clock Almost Non-Zeno Weighted Timed Games
Abstract
The Value Problem for weighted timed games (wtgs) consists in determining, given a two-player weighted timed game with a reachability objective and a rational threshold, whether or not the value of the game exceeds the threshold. When restrained to wtgs with non-negative weight, this problem is known to be undecidable for weighted timed games with three or more clocks, and decidable for one-clock wtgs. The Value Problem for two-clock non-negative wtgs, which remained stubbornly open for a decade, was recently shown to be undecidable. In this paper, we show that the Value Problem is decidable when considering two-clock almost non-Zeno wtgs.
Cite as
Isa Vialard. Deciding the Value of Two-Clock Almost Non-Zeno Weighted Timed Games. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 33:1-33:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{vialard:LIPIcs.CSL.2026.33,
author = {Vialard, Isa},
title = {{Deciding the Value of Two-Clock Almost Non-Zeno Weighted Timed Games}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {33:1--33:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.33},
URN = {urn:nbn:de:0030-drops-254580},
doi = {10.4230/LIPIcs.CSL.2026.33},
annote = {Keywords: Weighted timed games, decidability, real-time systems}
}
Document
Memory Requirements in Non-Zero-Sum Games
Abstract
The interaction between a system and the components modeling its environment is traditionally modeled by a multi-player game played on a finite graph. In zero-sum games, the players have conflicting objectives, and it is clear that increasing the memory of the environment players can only make it harder for the system to win. In non-zero-sum games, the objectives of the players may overlap. There, typical questions concern the stability of the game and the equilibria the players may reach. In particular, in rational synthesis (RS), the goal is to find an equilibrium that satisfies the objective of the system.
We study how the memory of the environment players may affect the existence of an RS solution. As we show, the picture is diverse, even when the objectives of all players are memoryless. On the one hand, when stability amounts to a Nash equilibrium (NE), then increasing the memory of the environment may only help the system to suggest an RS solution. On the other hand, when the notion of stability involves deviations by coalitions of environment players, for example in a strong Nash equilibrium (SNE), then increasing their memory may sometimes enable and sometimes prevent the existence of an RS solution. We study memory bounds for the players, showing that the memory required may be polynomial in an NE-RS solution and exponential in an SNE-RS solution. We also solve the SNE-RS problem, show that it is PSPACE-complete, and relate the differences between NE and SNE with the differences between cooperative and non-cooperative RS.
Cite as
Yoav Feinstein and Orna Kupferman. Memory Requirements in Non-Zero-Sum Games. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 34:1-34:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{feinstein_et_al:LIPIcs.CSL.2026.34,
author = {Feinstein, Yoav and Kupferman, Orna},
title = {{Memory Requirements in Non-Zero-Sum Games}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {34:1--34:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.34},
URN = {urn:nbn:de:0030-drops-254597},
doi = {10.4230/LIPIcs.CSL.2026.34},
annote = {Keywords: Non-Zero-Sum Games, Synthesis, Memory}
}
Document
Boolean Basis and Succinctness of Modal Logic via Hella-Vilander Games
Abstract
The Hella-Vilander game for modal logic is a model comparison game that captures the formula size necessary to separate sets of pointed Kripke structures. We introduce the ℳ-ON game as a modification of this game. Our game captures the necessary number of modal operators, i.e., ◇ and □ instead of formula size. We use our game to show that the bi-implication ↔, sometimes also called equivalence, enables us to write modal logic formula with significantly fewer modal operators. With this we show, that with bi-implications we can also write significantly shorter modal logic formulas. This result holds even if only special classes of Kripke structures are considered. To be more precise we show that there is an exponential succinctness gap between modal logic and its extension with bi-implication on the class of structures with a transitive and reflexive accessibility relation, as well as on the class of structures with a symmetrical and reflexive accessibility relation. Lastly we show that for the class of structures with a transitive and symmetrical accessibility relation this succinctness gap disappears.
Cite as
Sebastian Pfau. Boolean Basis and Succinctness of Modal Logic via Hella-Vilander Games. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 35:1-35:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{pfau:LIPIcs.CSL.2026.35,
author = {Pfau, Sebastian},
title = {{Boolean Basis and Succinctness of Modal Logic via Hella-Vilander Games}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {35:1--35:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.35},
URN = {urn:nbn:de:0030-drops-254600},
doi = {10.4230/LIPIcs.CSL.2026.35},
annote = {Keywords: succinctness, modal logic, model comparison games}
}
Document
A Game for Counting Logic Formula Size and an Application to Linear Orders
Abstract
Ehrenfeucht-Fraïssé (EF) games are a basic tool in finite model theory for proving definability lower bounds, with many applications in complexity theory and related areas. They have been applied to study various logics, giving insights on quantifier rank and other logical complexity measures. In this paper, we present an EF game to capture formula size in counting logic with a bounded number of variables. The game combines games introduced previously for counting logic quantifier rank due to Immerman and Lander, and for first-order formula size due to Adler and Immerman, and Hella and Väänänen. The game is used to prove an extension of a formula size lower bound of Grohe and Schweikardt for distinguishing linear orders, from 3-variable first-order logic to 3-variable counting logic.
Cite as
Grégoire Fournier and György Turán. A Game for Counting Logic Formula Size and an Application to Linear Orders. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 36:1-36:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{fournier_et_al:LIPIcs.CSL.2026.36,
author = {Fournier, Gr\'{e}goire and Tur\'{a}n, Gy\"{o}rgy},
title = {{A Game for Counting Logic Formula Size and an Application to Linear Orders}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {36:1--36:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.36},
URN = {urn:nbn:de:0030-drops-254612},
doi = {10.4230/LIPIcs.CSL.2026.36},
annote = {Keywords: Finite Model Theory, Logical Aspects of Computational Complexity}
}
Document
Towards the Type Safety of Pure Subtype Systems
Abstract
Hutchins' Pure Subtype Systems (PSS) offer a unified framework for types and terms, promising significant advancements in language design for features like dependent types and higher-order subtyping. However, the theory has been hampered by a critical gap: a proof of type safety has remained an open problem for over a decade. The original attempt to prove this property relied on the conjectured commutativity of two fundamental reduction relations, equivalence and subtyping. Proving transitivity elimination, however, requires this commutativity, a property that is notoriously difficult to establish for higher-order subtyping systems.
In this paper, we address this issue by introducing Machine-Based PSS (MPSS), a novel reformulation of the original system. MPSS integrates a continuation stack mechanism, reminiscent of the Krivine Abstract Machine, to keep track of arguments that are passed during function application, enabling more fine-grained reductions. This architectural change exposes crucial intermediate reduction steps that were absent in the original PSS. The primary contribution of our work is a direct proof that the equivalence and subtyping reductions in MPSS commute. This result formally establishes transitivity elimination, which is the cornerstone of the inversion lemma required for type safety. We conclude by outlining a pathway from our foundational result to a complete, type-safe system, thereby paving the way for the practical realization of PSS-based languages.
Cite as
Valentin Pasquale and Álvaro García-Pérez. Towards the Type Safety of Pure Subtype Systems. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 37:1-37:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{pasquale_et_al:LIPIcs.CSL.2026.37,
author = {Pasquale, Valentin and Garc{\'\i}a-P\'{e}rez, \'{A}lvaro},
title = {{Towards the Type Safety of Pure Subtype Systems}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {37:1--37:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.37},
URN = {urn:nbn:de:0030-drops-254626},
doi = {10.4230/LIPIcs.CSL.2026.37},
annote = {Keywords: Lambda calculus, Pure subtype systems, Dependent types, Higher-order subtyping, Type safety}
}
Document
The Biequivalence of Path Categories and Axiomatic Martin-Löf Type Theories
Abstract
The semantics of extensional type theory has an elegant categorical description: models of extensional =-types, 𝟙-types, and Σ-types are biequivalent to finitely complete categories, while adding Π-types yields locally Cartesian closed categories. We establish parallel results for axiomatic type theory, which includes systems like cubical type theory, where the computation rule of the =-types only holds as a propositional axiom instead of a definitional reduction. In particular, we prove that models of axiomatic =-types, and standard 𝟙- and Σ-types are biequivalent to certain path categories, while adding axiomatic Π-types yields dependent homotopy exponents.
This biequivalence simplifies axiomatic =-types, which are more intricate than extensional ones since they permit higher dimensional structure. Specifically, path categories use a primitive notion of equivalence instead of a direct reproduction of the syntactic elimination rules and computation axioms. We apply our correspondence to prove a coherence theorem: we show that these weak homotopical models can be turned into equivalent strict models of axiomatic type theory. In addition, we introduce a more modular notion, that of a display map path category, which only models axiomatic =-types by default, while leaving room to add other axiomatic type formers such as 𝟙-, Σ-, and Π-types.
Cite as
Daniël Otten and Matteo Spadetto. The Biequivalence of Path Categories and Axiomatic Martin-Löf Type Theories. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 38:1-38:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{otten_et_al:LIPIcs.CSL.2026.38,
author = {Otten, Dani\"{e}l and Spadetto, Matteo},
title = {{The Biequivalence of Path Categories and Axiomatic Martin-L\"{o}f Type Theories}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {38:1--38:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.38},
URN = {urn:nbn:de:0030-drops-254633},
doi = {10.4230/LIPIcs.CSL.2026.38},
annote = {Keywords: Axiomatic type theory, cubical type theory, propositional equality, biequivalence, display map categories, path categories, homotopy theory, coherence}
}
Document
A Canonical Form for Universe Levels in Impredicative Type Theory
Abstract
The 0-imax-successor algebra, where imax: ℕ × ℕ → ℕ is the function defined by imax(n, 0) = 0 and imax(n, S(m)) = max(n, S(m)), is used to represent universe levels in impredicative type theory, in particular with universe polymorphism which introduces level variables, so it is present in proof systems such as Rocq and Lean. In particular, we need to know when two elements of this algebra are equivalent, and we may also want to decide the inequality. In this article, we introduce a canonical form for the terms of this algebra, and we provide a canonization algorithm. It permits deciding level equivalence by checking the canonical form equality, and also permits easily checking if a level is smaller than another one.
Cite as
Yoan Géran. A Canonical Form for Universe Levels in Impredicative Type Theory. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 39:1-39:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{geran:LIPIcs.CSL.2026.39,
author = {G\'{e}ran, Yoan},
title = {{A Canonical Form for Universe Levels in Impredicative Type Theory}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {39:1--39:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.39},
URN = {urn:nbn:de:0030-drops-254640},
doi = {10.4230/LIPIcs.CSL.2026.39},
annote = {Keywords: universe levels, canonical form, impredicativity, imax algebra}
}
Document
The Groupoid-Syntax of Type Theory Is a Set
Abstract
Categories with families (CwFs) have been used to define the semantics of type theory in type theory. In the setting of Homotopy Type Theory (HoTT), one of the limitations of the traditional notion of CwFs is the requirement to set-truncate types, which excludes models based on univalent categories, such as the standard set model. To address this limitation, we introduce the concept of a Groupoid Category with Families (GCwF). This framework truncates types at the groupoid level and incorporates coherence equations, providing a natural extension of the CwF framework when starting from a 1-category.
We demonstrate that the initial GCwF for a type theory with a base family of sets and Π-types (groupoid-syntax) is set-truncated. Consequently, this allows us to utilize the conventional intrinsic syntax of type theory while enabling interpretations in semantically richer and more natural models. All constructions in this paper were formalised in Cubical Agda.
Cite as
Thorsten Altenkirch, Ambrus Kaposi, and Szumi Xie. The Groupoid-Syntax of Type Theory Is a Set. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 40:1-40:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{altenkirch_et_al:LIPIcs.CSL.2026.40,
author = {Altenkirch, Thorsten and Kaposi, Ambrus and Xie, Szumi},
title = {{The Groupoid-Syntax of Type Theory Is a Set}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {40:1--40:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.40},
URN = {urn:nbn:de:0030-drops-254650},
doi = {10.4230/LIPIcs.CSL.2026.40},
annote = {Keywords: Categorical models of type theory, category with families, groupoids, coherence, homotopy type theory}
}
Document
Weakly-Sparse and Strongly Flip-Flat Classes of Graphs Are Uniformly Almost-Wide
Abstract
In this work we take a step towards characterising strongly flip-flat classes of graphs. Strong flip-flatness appears to be the analogue of uniform almost-wideness in the setting of dense classes of graphs. We prove that strongly flip-flat classes of graphs that are weakly sparse are indeed uniformly almost-wide.
Cite as
Fatemeh Ghasemi, Julien Grange, Mamadou Moustapha Kanté, and Florent Madelaine. Weakly-Sparse and Strongly Flip-Flat Classes of Graphs Are Uniformly Almost-Wide. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 41:1-41:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{ghasemi_et_al:LIPIcs.CSL.2026.41,
author = {Ghasemi, Fatemeh and Grange, Julien and Kant\'{e}, Mamadou Moustapha and Madelaine, Florent},
title = {{Weakly-Sparse and Strongly Flip-Flat Classes of Graphs Are Uniformly Almost-Wide}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {41:1--41:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.41},
URN = {urn:nbn:de:0030-drops-254668},
doi = {10.4230/LIPIcs.CSL.2026.41},
annote = {Keywords: Almost-wide, Flip-flatness}
}
Document
Robustness of Constraint Automata for Description Logics with Concrete Domains
Abstract
Decidability or complexity issues about the consistency problem for description logics with concrete domains have already been analysed with tableaux-based or type elimination methods. Concrete domains in ontologies are essential to consider concrete objects and predefined relations. In this work, we expose an automata-based approach leading to the optimal upper bound ExpTime, that is designed by enriching the transitions with symbolic constraints. We show that the nonemptiness problem for such automata belongs to ExpTime if the concrete domains satisfy a few simple properties. Then, we provide a reduction from the consistency problem for ontologies, yielding ExpTime-membership. Thanks to the expressivity of constraint automata, the results are extended to additional ingredients such as inverse roles, functional role names and constraint assertions, while maintaining ExpTime-membership, which illustrates the robustness of the approach.
Cite as
Stéphane Demri and Tianwen Gu. Robustness of Constraint Automata for Description Logics with Concrete Domains. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 42:1-42:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{demri_et_al:LIPIcs.CSL.2026.42,
author = {Demri, St\'{e}phane and Gu, Tianwen},
title = {{Robustness of Constraint Automata for Description Logics with Concrete Domains}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {42:1--42:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.42},
URN = {urn:nbn:de:0030-drops-254679},
doi = {10.4230/LIPIcs.CSL.2026.42},
annote = {Keywords: Description logics, concrete domains, constraint automata, complexity}
}
Document
Kamp Theorem for Pomset Languages of Higher Dimensional Automata
Abstract
Temporal logics are a powerful tool to specify properties of computational systems. For concurrent programs, Higher Dimensional Automata (HDA) are a very expressive model of non-interleaving concurrency. HDA recognize languages of partially ordered multisets, or pomsets. Recent work has shown that Monadic Second Order (MSO) logic is as expressive as HDA for pomset languages. In the case of words, Kamp’s theorem states that First Order (FO) logic is as expressive as Linear Temporal Logic (LTL). In this paper, we extend this result to pomsets. To do so, we first investigate the class of pomset languages that are definable in FO. As expected, this is a strict subclass of MSO-definable languages. Then, we define a Linear Temporal Logic for pomsets (LTL_Poms), and show that it is equivalent to FO.
Cite as
Emily Clement, Enzo Erlich, and Jérémy Ledent. Kamp Theorem for Pomset Languages of Higher Dimensional Automata. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 43:1-43:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{clement_et_al:LIPIcs.CSL.2026.43,
author = {Clement, Emily and Erlich, Enzo and Ledent, J\'{e}r\'{e}my},
title = {{Kamp Theorem for Pomset Languages of Higher Dimensional Automata}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {43:1--43:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.43},
URN = {urn:nbn:de:0030-drops-254685},
doi = {10.4230/LIPIcs.CSL.2026.43},
annote = {Keywords: Higher dimensional automata, temporal logic, Kamp’s theorem}
}
Document
Minimal DFAs Witnessing Language Inequivalence
Abstract
We study small witnesses for the inequivalence of two regular languages. A natural witness is a distinguishing word, e.g. a word in exactly one of the two languages. We propose using more succinct witnesses in the form of witnessing DFAs. A witnessing DFA recognizes a subset of one of the languages and contains at least one distinguishing word. In this way the DFA expresses behaviour contained in the first language but not the second. We show witnessing DFAs can be used to present more concise witnesses for the inequivalence of two regular languages. We show that the decision problem for the existence of a witnessing DFA of certain size is NP-complete in general, and in P in the special case of unary DFAs. Besides these computational aspects, we study structural properties of witnessing DFAs. Not all languages can be a minimal witness. It turns out that minimal witnesses are exactly the languages that are not decomposable in the union of languages with smaller state-complexity, the so-called prime languages as studied earlier by Kupferman and Mosheiff.
Cite as
Jan Martens. Minimal DFAs Witnessing Language Inequivalence. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 44:1-44:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{martens:LIPIcs.CSL.2026.44,
author = {Martens, Jan},
title = {{Minimal DFAs Witnessing Language Inequivalence}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {44:1--44:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.44},
URN = {urn:nbn:de:0030-drops-254691},
doi = {10.4230/LIPIcs.CSL.2026.44},
annote = {Keywords: Deterministic Finite Automata, Language Inequivalence, DFA decomposition, Prime languages}
}
Document
Reasoning About Quality in Hyperproperties
Abstract
Hyperproperties allow one to specify properties of systems that inherently involve not single executions of the system, but several of them at once: observational determinism and non-inference are two examples of such properties used to study the security of systems. Logics like HyperLTL have been studied in the past to model check hyperproperties of systems. However, most of the time, requiring strict security properties is actually ineffective as systems do not meet such requirements. To overcome this issue, we introduce qualitative reasoning in HyperLTL, inspired by a similar work on LTL by Almagor, Boker and Kupferman [Almagor et al., 2016] where a formula has a value in the interval [0, 1], obtained by considering either a propositional quality (how much the specification is satisfied), or a temporal quality (when the specification is satisfied). We show decidability of the approximated model checking problem, as well as the model checking of large fragments.
Cite as
Samuel Graepler, Benjamin Monmege, and Jean-Marc Talbot. Reasoning About Quality in Hyperproperties. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 45:1-45:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{graepler_et_al:LIPIcs.CSL.2026.45,
author = {Graepler, Samuel and Monmege, Benjamin and Talbot, Jean-Marc},
title = {{Reasoning About Quality in Hyperproperties}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {45:1--45:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.45},
URN = {urn:nbn:de:0030-drops-254704},
doi = {10.4230/LIPIcs.CSL.2026.45},
annote = {Keywords: Hyperlogics, Automata-based model checking, Quantitative verification}
}
Document
Lax Modal Lambda Calculi
Abstract
Intuitionistic modal logics (IMLs) extend intuitionistic propositional logic with modalities such as the box and diamond connectives. Advances in the study of IMLs have inspired several applications in programming languages via the development of corresponding type theories with modalities. Until recently, IMLs with diamonds have been misunderstood as somewhat peculiar and unstable, causing the development of type theories with diamonds to lag behind type theories with boxes. In this article, we develop a family of typed-lambda calculi corresponding to sublogics of a peculiar IML with diamonds known as Lax logic. These calculi provide a modal logical foundation for various strong functors in typed-functional programming. We present possible-world and categorical semantics for these calculi and constructively prove normalization, equational completeness and proof-theoretic inadmissibility results. Our main results have been formalized using the proof assistant Agda.
Cite as
Nachiappan Valliappan. Lax Modal Lambda Calculi. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 46:1-46:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{valliappan:LIPIcs.CSL.2026.46,
author = {Valliappan, Nachiappan},
title = {{Lax Modal Lambda Calculi}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {46:1--46:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.46},
URN = {urn:nbn:de:0030-drops-254714},
doi = {10.4230/LIPIcs.CSL.2026.46},
annote = {Keywords: intuitionistic modal logic, typed lambda calculi, diamond modality}
}
Document
Useful Call-by-Value: A Semantic Interpretation via Quantitative Types
Abstract
Useful evaluation is an optimised evaluation mechanism for functional programming languages. It relies on representing terms with sharing and imposing a restricted notion of useful substitutions, that intuitively disallows copying subterms that do not contribute to the progress of the computation.
In particular, useful call-by-value evaluation optimises the standard call-by-value strategy by preserving its original semantics. This preservation result has been shown by means of syntactical rewriting techniques, difficult to adapt to alternative variants of the calculi at play.
In this work, we present the first semantic model of useful call-by-value evaluation through the non-idempotent intersection type system 𝒰. Our first contribution is a characterisation of termination for useful call-by-value evaluation via system 𝒰. That is, a term is typable in system 𝒰 if and only if it terminates in the useful call-by-value strategy. As a second contribution, we show that system 𝒰 provides a quantitative interpretation for useful call-by-value evaluation, offering exact step-count information for program evaluation. Our third contribution is that termination in call-by-value and useful call-by-value are equivalent. This ensures in particular that call-by-value, which is (potentially) erasing, and useful call-by-value, which is non-erasing, are observationally equivalent. Even though the specification of the operational semantics of useful evaluation is highly complex, system 𝒰 is notably simple. As far as we know, system 𝒰 is one of the scarce quantitative type systems capturing exactly the substitution step-count for variables and abstractions in an open call-by-value strategy.
Cite as
Pablo Barenbaum, Delia Kesner, and Mariana Milicich. Useful Call-by-Value: A Semantic Interpretation via Quantitative Types. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 47:1-47:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{barenbaum_et_al:LIPIcs.CSL.2026.47,
author = {Barenbaum, Pablo and Kesner, Delia and Milicich, Mariana},
title = {{Useful Call-by-Value: A Semantic Interpretation via Quantitative Types}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {47:1--47:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.47},
URN = {urn:nbn:de:0030-drops-254721},
doi = {10.4230/LIPIcs.CSL.2026.47},
annote = {Keywords: Lambda calculus, Evaluation strategies, Call-by-Value, Useful Evaluation, Intersection types, Quantitative models}
}
Document
Interpreting Lambda Calculus in Domain-Valued Random Variables
Abstract
We develop Boolean-valued domain theory and show how the lambda-calculus can be interpreted using domain-valued random variables. We focus on the reflexive domain construction rather than the language and its semantics. We develop the Boolean-valued set theory needed from scratch and then develop Boolean-valued domain theory on top of that. The notions of equality and partial order have to be given Boolean-valued interpretations; when we say that an equation is valid in the model we mean that its interpretation is the top element of the Boolean algebra.
Cite as
Robert Furber, Radu Mardare, Prakash Panangaden, and Dana Scott. Interpreting Lambda Calculus in Domain-Valued Random Variables. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 48:1-48:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{furber_et_al:LIPIcs.CSL.2026.48,
author = {Furber, Robert and Mardare, Radu and Panangaden, Prakash and Scott, Dana},
title = {{Interpreting Lambda Calculus in Domain-Valued Random Variables}},
booktitle = {34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
pages = {48:1--48:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-411-6},
ISSN = {1868-8969},
year = {2026},
volume = {363},
editor = {Guerrini, Stefano and K\"{o}nig, Barbara},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.48},
URN = {urn:nbn:de:0030-drops-254734},
doi = {10.4230/LIPIcs.CSL.2026.48},
annote = {Keywords: lambda calculus, domain theory, random variables}
}