32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 1-892, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@Proceedings{murano_et_al:LIPIcs.CSL.2024, title = {{LIPIcs, Volume 288, CSL 2024, Complete Volume}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {1--892}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024}, URN = {urn:nbn:de:0030-drops-196423}, doi = {10.4230/LIPIcs.CSL.2024}, annote = {Keywords: LIPIcs, Volume 288, CSL 2024, Complete Volume} }
32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{murano_et_al:LIPIcs.CSL.2024.0, author = {Murano, Aniello and Silva, Alexandra}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {0:i--0:xiv}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.0}, URN = {urn:nbn:de:0030-drops-196436}, doi = {10.4230/LIPIcs.CSL.2024.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} }
Maribel Fernández, Jean Goubault-Larrecq, and Delia Kesner. The Ackermann Award 2023. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 1:1-1:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{fernandez_et_al:LIPIcs.CSL.2024.1, author = {Fern\'{a}ndez, Maribel and Goubault-Larrecq, Jean and Kesner, Delia}, title = {{The Ackermann Award 2023}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {1:1--1:4}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.1}, URN = {urn:nbn:de:0030-drops-196446}, doi = {10.4230/LIPIcs.CSL.2024.1}, annote = {Keywords: lambda-calculus, computational complexity, geometry of interaction, abstract machines, intersection types} }
Balder ten Cate. Craig Interpolation for Decidable Fragments of First-Order Logic (Invited Talk). In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{tencate:LIPIcs.CSL.2024.2, author = {ten Cate, Balder}, title = {{Craig Interpolation for Decidable Fragments of First-Order Logic}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {2:1--2:2}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.2}, URN = {urn:nbn:de:0030-drops-196488}, doi = {10.4230/LIPIcs.CSL.2024.2}, annote = {Keywords: First-Order Logic, Decidable Fragments, Craig Interpolation} }
Georg Gottlob. Artificial Intelligence and Artificial Ignorance (Invited Talk). In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{gottlob:LIPIcs.CSL.2024.3, author = {Gottlob, Georg}, title = {{Artificial Intelligence and Artificial Ignorance}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {3:1--3:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.3}, URN = {urn:nbn:de:0030-drops-196459}, doi = {10.4230/LIPIcs.CSL.2024.3}, annote = {Keywords: AI applications, symbolic AI, sub-symbolic AI, AI usefulness, achievements of symbolic AI, achievements of machine learning, machine learning errors and mistakes, large language models, LLMs, LLM usefulness, LLM mistakes, inaccuracies} }
Barbara König. Approximating Fixpoints of Approximated Functions (Invited Talk). In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, p. 4:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{konig:LIPIcs.CSL.2024.4, author = {K\"{o}nig, Barbara}, title = {{Approximating Fixpoints of Approximated Functions}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {4:1--4:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.4}, URN = {urn:nbn:de:0030-drops-196469}, doi = {10.4230/LIPIcs.CSL.2024.4}, annote = {Keywords: fixpoints, approximation, Markov decision processes} }
Marta Kwiatkowska. Strategy Synthesis for Partially Observable Stochastic Games with Neural Perception Mechanisms (Invited Talk). In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 5:1-5:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{kwiatkowska:LIPIcs.CSL.2024.5, author = {Kwiatkowska, Marta}, title = {{Strategy Synthesis for Partially Observable Stochastic Games with Neural Perception Mechanisms}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {5:1--5:2}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.5}, URN = {urn:nbn:de:0030-drops-196471}, doi = {10.4230/LIPIcs.CSL.2024.5}, annote = {Keywords: Stochastic games, neural networks, formal verification, strategy synthesis} }
Moshe Y. Vardi. Logical Algorithmics: From Theory to Practice (Invited Talk). In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, p. 6:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{vardi:LIPIcs.CSL.2024.6, author = {Vardi, Moshe Y.}, title = {{Logical Algorithmics: From Theory to Practice}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {6:1--6:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.6}, URN = {urn:nbn:de:0030-drops-196494}, doi = {10.4230/LIPIcs.CSL.2024.6}, annote = {Keywords: Logic, Algorithms} }
Beniamino Accattoli. Semantic Bounds and Multi Types, Revisited. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 7:1-7:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{accattoli:LIPIcs.CSL.2024.7, author = {Accattoli, Beniamino}, title = {{Semantic Bounds and Multi Types, Revisited}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {7:1--7:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.7}, URN = {urn:nbn:de:0030-drops-196504}, doi = {10.4230/LIPIcs.CSL.2024.7}, annote = {Keywords: Lambda calculus, intersection types, denotational semantics, linear logic} }
Matteo Acclavio, Gianluca Curzi, and Giulio Guerrieri. Infinitary Cut-Elimination via Finite Approximations. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 8:1-8:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{acclavio_et_al:LIPIcs.CSL.2024.8, author = {Acclavio, Matteo and Curzi, Gianluca and Guerrieri, Giulio}, title = {{Infinitary Cut-Elimination via Finite Approximations}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {8:1--8:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.8}, URN = {urn:nbn:de:0030-drops-196510}, doi = {10.4230/LIPIcs.CSL.2024.8}, annote = {Keywords: cut-elimination, non-wellfounded proofs, parsimonious logic, linear logic, proof theory, approximation, sequent calculus, non-uniform proofs} }
Veeti Ahvonen, Damian Heiman, and Antti Kuusisto. Descriptive Complexity for Neural Networks via Boolean Networks. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 9:1-9:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{ahvonen_et_al:LIPIcs.CSL.2024.9, author = {Ahvonen, Veeti and Heiman, Damian and Kuusisto, Antti}, title = {{Descriptive Complexity for Neural Networks via Boolean Networks}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {9:1--9:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.9}, URN = {urn:nbn:de:0030-drops-196528}, doi = {10.4230/LIPIcs.CSL.2024.9}, annote = {Keywords: Descriptive complexity, neural networks, Boolean networks, floating-point arithmetic, logic} }
Melissa Antonelli, Ugo Dal Lago, Davide Davoli, Isabel Oitavem, and Paolo Pistone. Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{antonelli_et_al:LIPIcs.CSL.2024.10, author = {Antonelli, Melissa and Dal Lago, Ugo and Davoli, Davide and Oitavem, Isabel and Pistone, Paolo}, title = {{Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {10:1--10:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.10}, URN = {urn:nbn:de:0030-drops-196538}, doi = {10.4230/LIPIcs.CSL.2024.10}, annote = {Keywords: Bounded Arithmetic, Randomized Computation, Implicit Computational Complexity} }
Quentin Aristote. Active Learning of Deterministic Transducers with Outputs in Arbitrary Monoids. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 11:1-11:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{aristote:LIPIcs.CSL.2024.11, author = {Aristote, Quentin}, title = {{Active Learning of Deterministic Transducers with Outputs in Arbitrary Monoids}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {11:1--11:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.11}, URN = {urn:nbn:de:0030-drops-196545}, doi = {10.4230/LIPIcs.CSL.2024.11}, annote = {Keywords: transducers, monoids, active learning, category theory} }
Anita Badyl and Paweł Parys. Extending the WMSO+U Logic with Quantification over Tuples. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{badyl_et_al:LIPIcs.CSL.2024.12, author = {Badyl, Anita and Parys, Pawe{\l}}, title = {{Extending the WMSO+U Logic with Quantification over Tuples}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {12:1--12:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.12}, URN = {urn:nbn:de:0030-drops-196557}, doi = {10.4230/LIPIcs.CSL.2024.12}, annote = {Keywords: Boundedness, logic, decidability, expressivity, recursion schemes} }
Philippe Balbiani, Han Gao, Çiğdem Gencer, and Nicola Olivetti. A Natural Intuitionistic Modal Logic: Axiomatization and Bi-Nested Calculus. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 13:1-13:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{balbiani_et_al:LIPIcs.CSL.2024.13, author = {Balbiani, Philippe and Gao, Han and Gencer, \c{C}i\u{g}dem and Olivetti, Nicola}, title = {{A Natural Intuitionistic Modal Logic: Axiomatization and Bi-Nested Calculus}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {13:1--13:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.13}, URN = {urn:nbn:de:0030-drops-196565}, doi = {10.4230/LIPIcs.CSL.2024.13}, annote = {Keywords: Intuitionistic Modal Logic, Axiomatization, Completeness, Sequent Calculus} }
Davide Barbarossa and Paolo Pistone. Tropical Mathematics and the Lambda-Calculus I: Metric and Differential Analysis of Effectful Programs. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 14:1-14:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{barbarossa_et_al:LIPIcs.CSL.2024.14, author = {Barbarossa, Davide and Pistone, Paolo}, title = {{Tropical Mathematics and the Lambda-Calculus I: Metric and Differential Analysis of Effectful Programs}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {14:1--14:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.14}, URN = {urn:nbn:de:0030-drops-196577}, doi = {10.4230/LIPIcs.CSL.2024.14}, annote = {Keywords: Relational semantics, Differential lambda-calculus, Tropical semiring, Program metrics, Lawvere quantale} }
Fausto Barbero and Jonni Virtema. Expressivity Landscape for Logics with Probabilistic Interventionist Counterfactuals. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 15:1-15:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{barbero_et_al:LIPIcs.CSL.2024.15, author = {Barbero, Fausto and Virtema, Jonni}, title = {{Expressivity Landscape for Logics with Probabilistic Interventionist Counterfactuals}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {15:1--15:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.15}, URN = {urn:nbn:de:0030-drops-196583}, doi = {10.4230/LIPIcs.CSL.2024.15}, annote = {Keywords: Interventionist counterfactuals, Multiteam semantics, Causation, Probability logic, Linear inequalities, Expressive power} }
Stefano Berardi, Gabriele Buriola, and Peter Schuster. A General Constructive Form of Higman’s Lemma. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{berardi_et_al:LIPIcs.CSL.2024.16, author = {Berardi, Stefano and Buriola, Gabriele and Schuster, Peter}, title = {{A General Constructive Form of Higman’s Lemma}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {16:1--16:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.16}, URN = {urn:nbn:de:0030-drops-196599}, doi = {10.4230/LIPIcs.CSL.2024.16}, annote = {Keywords: intuitionistic logic, constructive mathematics, formal proof, inductive predicate, bar induction, well quasi-order, Higman’s lemma} }
Manon Blanc and Olivier Bournez. Quantifiying the Robustness of Dynamical Systems. Relating Time and Space to Length and Precision. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 17:1-17:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{blanc_et_al:LIPIcs.CSL.2024.17, author = {Blanc, Manon and Bournez, Olivier}, title = {{Quantifiying the Robustness of Dynamical Systems. Relating Time and Space to Length and Precision}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {17:1--17:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.17}, URN = {urn:nbn:de:0030-drops-196609}, doi = {10.4230/LIPIcs.CSL.2024.17}, annote = {Keywords: Computability, Complexity theory, Computable analysis, Verification, Decision, Robustness, Dynamical Systems, Models of computation, Analogue Computations} }
Benjamin Bordais, Patricia Bouyer, and Stéphane Le Roux. From Local to Global Optimality in Concurrent Parity Games. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 18:1-18:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{bordais_et_al:LIPIcs.CSL.2024.18, author = {Bordais, Benjamin and Bouyer, Patricia and Le Roux, St\'{e}phane}, title = {{From Local to Global Optimality in Concurrent Parity Games}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {18:1--18:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.18}, URN = {urn:nbn:de:0030-drops-196612}, doi = {10.4230/LIPIcs.CSL.2024.18}, annote = {Keywords: Game forms, stochastic games, parity games, Blackwell/Martin values} }
Sophie Brinke, Erich Grädel, and Lovro Mrkonjić. Ehrenfeucht-Fraïssé Games in Semiring Semantics. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 19:1-19:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{brinke_et_al:LIPIcs.CSL.2024.19, author = {Brinke, Sophie and Gr\"{a}del, Erich and Mrkonji\'{c}, Lovro}, title = {{Ehrenfeucht-Fra\"{i}ss\'{e} Games in Semiring Semantics}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {19:1--19:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.19}, URN = {urn:nbn:de:0030-drops-196623}, doi = {10.4230/LIPIcs.CSL.2024.19}, annote = {Keywords: Semiring semantics, elementary equivalence, Ehrenfeucht-Fra\"{i}ss\'{e} games} }
Alexandre Clément, Noé Delorme, Simon Perdrix, and Renaud Vilmart. Quantum Circuit Completeness: Extensions and Simplifications. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 20:1-20:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{clement_et_al:LIPIcs.CSL.2024.20, author = {Cl\'{e}ment, Alexandre and Delorme, No\'{e} and Perdrix, Simon and Vilmart, Renaud}, title = {{Quantum Circuit Completeness: Extensions and Simplifications}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {20:1--20:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.20}, URN = {urn:nbn:de:0030-drops-196639}, doi = {10.4230/LIPIcs.CSL.2024.20}, annote = {Keywords: Quantum Circuits, Completeness, Graphical Language} }
Geoffrey Cruttwell and Jean-Simon Pacaud Lemay. Reverse Tangent Categories. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 21:1-21:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{cruttwell_et_al:LIPIcs.CSL.2024.21, author = {Cruttwell, Geoffrey and Lemay, Jean-Simon Pacaud}, title = {{Reverse Tangent Categories}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {21:1--21:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.21}, URN = {urn:nbn:de:0030-drops-196644}, doi = {10.4230/LIPIcs.CSL.2024.21}, annote = {Keywords: Tangent Categories, Reverse Tangent Categories, Reverse Differential Categories, Categorical Machine Learning} }
Anupam Das, Iris van der Giessen, and Sonia Marin. Intuitionistic Gödel-Löb Logic, à la Simpson: Labelled Systems and Birelational Semantics. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{das_et_al:LIPIcs.CSL.2024.22, author = {Das, Anupam and van der Giessen, Iris and Marin, Sonia}, title = {{Intuitionistic G\"{o}del-L\"{o}b Logic, \`{a} la Simpson: Labelled Systems and Birelational Semantics}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {22:1--22:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.22}, URN = {urn:nbn:de:0030-drops-196654}, doi = {10.4230/LIPIcs.CSL.2024.22}, annote = {Keywords: provability logic, proof theory, intuitionistic modal logic, cyclic proofs, non-wellfounded proofs, proof search, cut-elimination, labelled sequents} }
Anuj Dawar and Lauri Hella. Quantifiers Closed Under Partial Polymorphisms. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 23:1-23:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{dawar_et_al:LIPIcs.CSL.2024.23, author = {Dawar, Anuj and Hella, Lauri}, title = {{Quantifiers Closed Under Partial Polymorphisms}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {23:1--23:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.23}, URN = {urn:nbn:de:0030-drops-196662}, doi = {10.4230/LIPIcs.CSL.2024.23}, annote = {Keywords: generalized quantifiers, constraint satisfaction problems, pebble games, finite variable logics, descriptive complexity theory} }
Tom van Dijk, Georg Loho, and Matthew T. Maat. The Worst-Case Complexity of Symmetric Strategy Improvement. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{vandijk_et_al:LIPIcs.CSL.2024.24, author = {van Dijk, Tom and Loho, Georg and Maat, Matthew T.}, title = {{The Worst-Case Complexity of Symmetric Strategy Improvement}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {24:1--24:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.24}, URN = {urn:nbn:de:0030-drops-196672}, doi = {10.4230/LIPIcs.CSL.2024.24}, annote = {Keywords: Parity game, Mean payoff game, Symmetric strategy improvement, Strategy improvement, Worst-case complexity} }
Matt Earnshaw, James Hefford, and Mario Román. The Produoidal Algebra of Process Decomposition. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{earnshaw_et_al:LIPIcs.CSL.2024.25, author = {Earnshaw, Matt and Hefford, James and Rom\'{a}n, Mario}, title = {{The Produoidal Algebra of Process Decomposition}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {25:1--25:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.25}, URN = {urn:nbn:de:0030-drops-196688}, doi = {10.4230/LIPIcs.CSL.2024.25}, annote = {Keywords: monoidal categories, profunctors, lenses, duoidal categories} }
Eldar Fischer and Johann A. Makowsky. Extensions and Limits of the Specker-Blatter Theorem. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{fischer_et_al:LIPIcs.CSL.2024.26, author = {Fischer, Eldar and Makowsky, Johann A.}, title = {{Extensions and Limits of the Specker-Blatter Theorem}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {26:1--26:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.26}, URN = {urn:nbn:de:0030-drops-196694}, doi = {10.4230/LIPIcs.CSL.2024.26}, annote = {Keywords: Specker-Blatter Theorem, Monadic Second Order Logic, MC-finiteness} }
Eva Fluck, Tim Seppelt, and Gian Luca Spitzer. Going Deep and Going Wide: Counting Logic and Homomorphism Indistinguishability over Graphs of Bounded Treedepth and Treewidth. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 27:1-27:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{fluck_et_al:LIPIcs.CSL.2024.27, author = {Fluck, Eva and Seppelt, Tim and Spitzer, Gian Luca}, title = {{Going Deep and Going Wide: Counting Logic and Homomorphism Indistinguishability over Graphs of Bounded Treedepth and Treewidth}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {27:1--27:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.27}, URN = {urn:nbn:de:0030-drops-196704}, doi = {10.4230/LIPIcs.CSL.2024.27}, annote = {Keywords: Treewidth, treedepth, homomorphism indistinguishability, counting first-order logic} }
Laura Fontanella, Guillaume Geoffroy, and Richard Matthews. Realizability Models for Large Cardinals. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 28:1-28:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{fontanella_et_al:LIPIcs.CSL.2024.28, author = {Fontanella, Laura and Geoffroy, Guillaume and Matthews, Richard}, title = {{Realizability Models for Large Cardinals}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {28:1--28:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.28}, URN = {urn:nbn:de:0030-drops-196715}, doi = {10.4230/LIPIcs.CSL.2024.28}, annote = {Keywords: Logic, Classical Realizability, Set Theory, Large Cardinals} }
Yannick Forster, Dominik Kirst, and Niklas Mück. The Kleene-Post and Post’s Theorem in the Calculus of Inductive Constructions. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 29:1-29:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{forster_et_al:LIPIcs.CSL.2024.29, author = {Forster, Yannick and Kirst, Dominik and M\"{u}ck, Niklas}, title = {{The Kleene-Post and Post’s Theorem in the Calculus of Inductive Constructions}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {29:1--29:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.29}, URN = {urn:nbn:de:0030-drops-196728}, doi = {10.4230/LIPIcs.CSL.2024.29}, annote = {Keywords: Constructive mathematics, Computability theory, Logical foundations, Constructive type theory, Interactive theorem proving, Coq proof assistant} }
Éric Goubault, Roman Kniazev, and Jérémy Ledent. A Many-Sorted Epistemic Logic for Chromatic Hypergraphs. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 30:1-30:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{goubault_et_al:LIPIcs.CSL.2024.30, author = {Goubault, \'{E}ric and Kniazev, Roman and Ledent, J\'{e}r\'{e}my}, title = {{A Many-Sorted Epistemic Logic for Chromatic Hypergraphs}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {30:1--30:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.30}, URN = {urn:nbn:de:0030-drops-196730}, doi = {10.4230/LIPIcs.CSL.2024.30}, annote = {Keywords: Modal logics, epistemic logics, multi-agent systems, hypergraphs} }
Mario Grobler, Leif Sabellek, and Sebastian Siebertz. Remarks on Parikh-Recognizable Omega-languages. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 31:1-31:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{grobler_et_al:LIPIcs.CSL.2024.31, author = {Grobler, Mario and Sabellek, Leif and Siebertz, Sebastian}, title = {{Remarks on Parikh-Recognizable Omega-languages}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {31:1--31:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.31}, URN = {urn:nbn:de:0030-drops-196743}, doi = {10.4230/LIPIcs.CSL.2024.31}, annote = {Keywords: Parikh automata, blind counter machines, infinite words, B\"{u}chi’s theorem} }
Julian Gutierrez, Anthony W. Lin, Muhammad Najib, Thomas Steeples, and Michael Wooldridge. Characterising and Verifying the Core in Concurrent Multi-Player Mean-Payoff Games. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 32:1-32:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{gutierrez_et_al:LIPIcs.CSL.2024.32, author = {Gutierrez, Julian and Lin, Anthony W. and Najib, Muhammad and Steeples, Thomas and Wooldridge, Michael}, title = {{Characterising and Verifying the Core in Concurrent Multi-Player Mean-Payoff Games}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {32:1--32:25}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.32}, URN = {urn:nbn:de:0030-drops-196752}, doi = {10.4230/LIPIcs.CSL.2024.32}, annote = {Keywords: Concurrent games, multi-agent systems, temporal logic, game theory} }
Luisa Herrmann, Vincent Peth, and Sebastian Rudolph. Decidable (Ac)counting with Parikh and Muller: Adding Presburger Arithmetic to Monadic Second-Order Logic over Tree-Interpretable Structures. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 33:1-33:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{herrmann_et_al:LIPIcs.CSL.2024.33, author = {Herrmann, Luisa and Peth, Vincent and Rudolph, Sebastian}, title = {{Decidable (Ac)counting with Parikh and Muller: Adding Presburger Arithmetic to Monadic Second-Order Logic over Tree-Interpretable Structures}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {33:1--33:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.33}, URN = {urn:nbn:de:0030-drops-196768}, doi = {10.4230/LIPIcs.CSL.2024.33}, annote = {Keywords: MSO, BAPA, Parikh-Muller tree automata, decidability, MSO-interpretations} }
Alexander Kozachinskiy. Energy Games over Totally Ordered Groups. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 34:1-34:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{kozachinskiy:LIPIcs.CSL.2024.34, author = {Kozachinskiy, Alexander}, title = {{Energy Games over Totally Ordered Groups}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {34:1--34:12}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.34}, URN = {urn:nbn:de:0030-drops-196778}, doi = {10.4230/LIPIcs.CSL.2024.34}, annote = {Keywords: Games on graphs, half-positionality, ordered groups} }
François Laroussinie, Loriane Leclercq, and Arnaud Sangnier. QLTL Model-Checking. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 35:1-35:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{laroussinie_et_al:LIPIcs.CSL.2024.35, author = {Laroussinie, Fran\c{c}ois and Leclercq, Loriane and Sangnier, Arnaud}, title = {{QLTL Model-Checking}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {35:1--35:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.35}, URN = {urn:nbn:de:0030-drops-196783}, doi = {10.4230/LIPIcs.CSL.2024.35}, annote = {Keywords: Quantified Linear-time temporal logic, Model-cheking, Verification, Automata theory} }
Moritz Lichter, Benedikt Pago, and Tim Seppelt. Limitations of Game Comonads for Invertible-Map Equivalence via Homomorphism Indistinguishability. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 36:1-36:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{lichter_et_al:LIPIcs.CSL.2024.36, author = {Lichter, Moritz and Pago, Benedikt and Seppelt, Tim}, title = {{Limitations of Game Comonads for Invertible-Map Equivalence via Homomorphism Indistinguishability}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {36:1--36:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.36}, URN = {urn:nbn:de:0030-drops-196799}, doi = {10.4230/LIPIcs.CSL.2024.36}, annote = {Keywords: finite model theory, graph isomorphism, linear-algebraic logic, homomorphism indistinguishability, game comonads, invertible-map equivalence} }
Salvador Lucas. Confluence of Conditional Rewriting Modulo. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 37:1-37:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{lucas:LIPIcs.CSL.2024.37, author = {Lucas, Salvador}, title = {{Confluence of Conditional Rewriting Modulo}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {37:1--37:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.37}, URN = {urn:nbn:de:0030-drops-196809}, doi = {10.4230/LIPIcs.CSL.2024.37}, annote = {Keywords: Conditional rewriting, Confluence, Program analysis} }
Assia Mahboubi and Matthieu Piquerez. A First Order Theory of Diagram Chasing. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 38:1-38:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{mahboubi_et_al:LIPIcs.CSL.2024.38, author = {Mahboubi, Assia and Piquerez, Matthieu}, title = {{A First Order Theory of Diagram Chasing}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {38:1--38:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.38}, URN = {urn:nbn:de:0030-drops-196817}, doi = {10.4230/LIPIcs.CSL.2024.38}, annote = {Keywords: Diagram chasing, formal proofs, abelian categories, decidability} }
Rasmus Ejlers Møgelberg and Maaike Annebet Zwart. What Monads Can and Cannot Do with a Bit of Extra Time. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 39:1-39:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{mogelberg_et_al:LIPIcs.CSL.2024.39, author = {M{\o}gelberg, Rasmus Ejlers and Zwart, Maaike Annebet}, title = {{What Monads Can and Cannot Do with a Bit of Extra Time}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {39:1--39:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.39}, URN = {urn:nbn:de:0030-drops-196823}, doi = {10.4230/LIPIcs.CSL.2024.39}, annote = {Keywords: Delay Monad, Monad Compositions, Distributive Laws, Guarded Recursion, Type Theory} }
Vincent Moreau and Lê Thành Dũng (Tito) Nguyễn. Syntactically and Semantically Regular Languages of λ-Terms Coincide Through Logical Relations. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 40:1-40:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{moreau_et_al:LIPIcs.CSL.2024.40, author = {Moreau, Vincent and Nguy\~{ê}n, L\^{e} Th\`{a}nh D\~{u}ng (Tito)}, title = {{Syntactically and Semantically Regular Languages of \lambda-Terms Coincide Through Logical Relations}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {40:1--40:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.40}, URN = {urn:nbn:de:0030-drops-196831}, doi = {10.4230/LIPIcs.CSL.2024.40}, annote = {Keywords: regular languages, simple types, denotational semantics, logical relations} }
Antoine Mottet. Promise and Infinite-Domain Constraint Satisfaction. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 41:1-41:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{mottet:LIPIcs.CSL.2024.41, author = {Mottet, Antoine}, title = {{Promise and Infinite-Domain Constraint Satisfaction}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {41:1--41:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.41}, URN = {urn:nbn:de:0030-drops-196842}, doi = {10.4230/LIPIcs.CSL.2024.41}, annote = {Keywords: promise constraint satisfaction problems, polymorphisms, homogeneous structures, first-order logic} }
Satoshi Nakata. Local Operators in Topos Theory and Separation of Semi-Classical Axioms in Intuitionistic Arithmetic. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 42:1-42:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{nakata:LIPIcs.CSL.2024.42, author = {Nakata, Satoshi}, title = {{Local Operators in Topos Theory and Separation of Semi-Classical Axioms in Intuitionistic Arithmetic}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {42:1--42:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.42}, URN = {urn:nbn:de:0030-drops-196859}, doi = {10.4230/LIPIcs.CSL.2024.42}, annote = {Keywords: local operator, elementary topos, effective topos, realizability, intuitionistic arithmetic} }
Federico Olimpieri. Coherence by Normalization for Linear Multicategorical Structures. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 43:1-43:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{olimpieri:LIPIcs.CSL.2024.43, author = {Olimpieri, Federico}, title = {{Coherence by Normalization for Linear Multicategorical Structures}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {43:1--43:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.43}, URN = {urn:nbn:de:0030-drops-196865}, doi = {10.4230/LIPIcs.CSL.2024.43}, annote = {Keywords: Coherence, Linear Multicategories, Resource Calculi, Normalization} }
Daniël Otten and Benno van den Berg. Conservativity of Type Theory over Higher-Order Arithmetic. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 44:1-44:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{otten_et_al:LIPIcs.CSL.2024.44, author = {Otten, Dani\"{e}l and van den Berg, Benno}, title = {{Conservativity of Type Theory over Higher-Order Arithmetic}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {44:1--44:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.44}, URN = {urn:nbn:de:0030-drops-196873}, doi = {10.4230/LIPIcs.CSL.2024.44}, annote = {Keywords: Conservativity, Arithmetic, Realizability, Calculus of Inductive Constructions} }
Thomas Place and Marc Zeitoun. A Generic Characterization of Generalized Unary Temporal Logic and Two-Variable First-Order Logic. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 45:1-45:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{place_et_al:LIPIcs.CSL.2024.45, author = {Place, Thomas and Zeitoun, Marc}, title = {{A Generic Characterization of Generalized Unary Temporal Logic and Two-Variable First-Order Logic}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {45:1--45:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.45}, URN = {urn:nbn:de:0030-drops-196888}, doi = {10.4230/LIPIcs.CSL.2024.45}, annote = {Keywords: Classes of regular languages, Generalized unary temporal logic, Generalized two-variable first-order logic, Generic decidable characterizations, Membership, Separation} }
Daniel Stan, Muhammad Najib, Anthony Widjaja Lin, and Parosh Aziz Abdulla. Concurrent Stochastic Lossy Channel Games. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 46:1-46:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{stan_et_al:LIPIcs.CSL.2024.46, author = {Stan, Daniel and Najib, Muhammad and Lin, Anthony Widjaja and Abdulla, Parosh Aziz}, title = {{Concurrent Stochastic Lossy Channel Games}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {46:1--46:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.46}, URN = {urn:nbn:de:0030-drops-196894}, doi = {10.4230/LIPIcs.CSL.2024.46}, annote = {Keywords: concurrent, games, stochastic, lossy channels, wqo, finite attractor property, cooperative, core, Nash equilibrium} }
Jonathan Sterling, Daniel Gratzer, and Lars Birkedal. Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 47:1-47:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{sterling_et_al:LIPIcs.CSL.2024.47, author = {Sterling, Jonathan and Gratzer, Daniel and Birkedal, Lars}, title = {{Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {47:1--47:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.47}, URN = {urn:nbn:de:0030-drops-196901}, doi = {10.4230/LIPIcs.CSL.2024.47}, annote = {Keywords: univalent foundations, homotopy type theory, impredicative encodings, synthetic guarded domain theory, guarded recursion, higher-order store, reference types} }
Marius Tritschler. Guarded Hybrid Team Logics. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 48:1-48:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{tritschler:LIPIcs.CSL.2024.48, author = {Tritschler, Marius}, title = {{Guarded Hybrid Team Logics}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {48:1--48:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.48}, URN = {urn:nbn:de:0030-drops-196919}, doi = {10.4230/LIPIcs.CSL.2024.48}, annote = {Keywords: Team semantics, guarded logics, expressiveness, model checking games} }
Feedback for Dagstuhl Publishing