@Proceedings{baier_et_al:LIPIcs.CSL.2021, title = {{LIPIcs, Volume 183, CSL 2021, Complete Volume}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {1--734}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021}, URN = {urn:nbn:de:0030-drops-134339}, doi = {10.4230/LIPIcs.CSL.2021}, annote = {Keywords: LIPIcs, Volume 183, CSL 2021, Complete Volume} } @InProceedings{baier_et_al:LIPIcs.CSL.2021.0, author = {Baier, Christel and Goubault-Larrecq, Jean}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {0:i--0:xx}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.0}, URN = {urn:nbn:de:0030-drops-134348}, doi = {10.4230/LIPIcs.CSL.2021.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} } @InProceedings{klin:LIPIcs.CSL.2021.1, author = {Klin, Bartek}, title = {{\mu-Calculi with Atoms}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {1:1--1:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.1}, URN = {urn:nbn:de:0030-drops-134358}, doi = {10.4230/LIPIcs.CSL.2021.1}, annote = {Keywords: modal \mu-calculus, sets with atoms} } @InProceedings{mahboubi:LIPIcs.CSL.2021.2, author = {Mahboubi, Assia}, title = {{Mathematical Structures in Dependent Type Theory}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {2:1--2:3}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.2}, URN = {urn:nbn:de:0030-drops-134361}, doi = {10.4230/LIPIcs.CSL.2021.2}, annote = {Keywords: Mathematical structures, formalized mathematics, dependent type theory} } @InProceedings{schmitz:LIPIcs.CSL.2021.3, author = {Schmitz, Sylvain}, title = {{Branching in Well-Structured Transition Systems}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {3:1--3:3}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.3}, URN = {urn:nbn:de:0030-drops-134377}, doi = {10.4230/LIPIcs.CSL.2021.3}, annote = {Keywords: fast-growing complexity, well-structured transition system} } @InProceedings{westrick:LIPIcs.CSL.2021.4, author = {Westrick, Linda}, title = {{Borel Sets in Reverse Mathematics}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {4:1--4:2}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.4}, URN = {urn:nbn:de:0030-drops-134387}, doi = {10.4230/LIPIcs.CSL.2021.4}, annote = {Keywords: Borel sets, reverse mathematics, measure, category} } @InProceedings{abramsky_et_al:LIPIcs.CSL.2021.5, author = {Abramsky, Samson and Barbosa, Rui Soares}, title = {{The Logic of Contextuality}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {5:1--5:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.5}, URN = {urn:nbn:de:0030-drops-134394}, doi = {10.4230/LIPIcs.CSL.2021.5}, annote = {Keywords: partial Boolean algebras, contextuality, exclusivity principles, Kochen-Specker paradoxes, tensor product} } @InProceedings{accattoli_et_al:LIPIcs.CSL.2021.6, author = {Accattoli, Beniamino and Faggian, Claudia and Guerrieri, Giulio}, title = {{Factorize Factorization}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {6:1--6:25}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.6}, URN = {urn:nbn:de:0030-drops-134407}, doi = {10.4230/LIPIcs.CSL.2021.6}, annote = {Keywords: Lambda Calculus, Rewriting, Reduction Strategies, Factorization} } @InProceedings{aceto_et_al:LIPIcs.CSL.2021.7, author = {Aceto, Luca and Achilleos, Antonis and Francalanza, Adrian and Ing\'{o}lfsd\'{o}ttir, Anna and Lehtinen, Karoliina}, title = {{The Best a Monitor Can Do}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {7:1--7:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.7}, URN = {urn:nbn:de:0030-drops-134416}, doi = {10.4230/LIPIcs.CSL.2021.7}, annote = {Keywords: monitorability, branching-time logics, runtime verification} } @InProceedings{aceto_et_al:LIPIcs.CSL.2021.8, author = {Aceto, Luca and Castiglioni, Valentina and Fokkink, Wan and Ing\'{o}lfsd\'{o}ttir, Anna and Luttik, Bas}, title = {{Are Two Binary Operators Necessary to Finitely Axiomatise Parallel Composition?}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {8:1--8:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.8}, URN = {urn:nbn:de:0030-drops-134425}, doi = {10.4230/LIPIcs.CSL.2021.8}, annote = {Keywords: Equational logic, CCS, bisimulation, parallel composition, non-finitely based algebras} } @InProceedings{arnold_et_al:LIPIcs.CSL.2021.9, author = {Arnold, Andr\'{e} and Niwi\'{n}ski, Damian and Parys, Pawe{\l}}, title = {{A Quasi-Polynomial Black-Box Algorithm for Fixed Point Evaluation}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {9:1--9:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.9}, URN = {urn:nbn:de:0030-drops-134430}, doi = {10.4230/LIPIcs.CSL.2021.9}, annote = {Keywords: Mu-calculus, Parity games, Quasi-polynomial time, Black-box algorithm} } @InProceedings{vanbergerem_et_al:LIPIcs.CSL.2021.10, author = {van Bergerem, Steffen and Schweikardt, Nicole}, title = {{Learning Concepts Described By Weight Aggregation Logic}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {10:1--10:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.10}, URN = {urn:nbn:de:0030-drops-134447}, doi = {10.4230/LIPIcs.CSL.2021.10}, annote = {Keywords: first-order definable concept learning, agnostic probably approximately correct learning, classification problems, locality, Feferman-Vaught decomposition, Gaifman normal form, first-order logic with counting, weight aggregation logic} } @InProceedings{bickford_et_al:LIPIcs.CSL.2021.11, author = {Bickford, Mark and Cohen, Liron and Constable, Robert L. and Rahli, Vincent}, title = {{Open Bar - a Brouwerian Intuitionistic Logic with a Pinch of Excluded Middle}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {11:1--11:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.11}, URN = {urn:nbn:de:0030-drops-134455}, doi = {10.4230/LIPIcs.CSL.2021.11}, annote = {Keywords: Intuitionism, Extensional type theory, Constructive Type Theory, Realizability, Choice sequences, Classical Logic, Law of Excluded Middle, Theorem proving, Coq} } @InProceedings{boker_et_al:LIPIcs.CSL.2021.12, author = {Boker, Udi and Hefetz, Guy}, title = {{Discounted-Sum Automata with Multiple Discount Factors}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {12:1--12:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.12}, URN = {urn:nbn:de:0030-drops-134468}, doi = {10.4230/LIPIcs.CSL.2021.12}, annote = {Keywords: Automata, Discounted-sum, Quantitative verification, NMDA, NDA} } @InProceedings{bollig_et_al:LIPIcs.CSL.2021.13, author = {Bollig, Benedikt and Ryabinin, Fedor and Sangnier, Arnaud}, title = {{Reachability in Distributed Memory Automata}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {13:1--13:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.13}, URN = {urn:nbn:de:0030-drops-134472}, doi = {10.4230/LIPIcs.CSL.2021.13}, annote = {Keywords: Distributed algorithms, Atomic snapshot objects, Register automata, Reachability} } @InProceedings{broda:LIPIcs.CSL.2021.14, author = {Broda, Sabine}, title = {{Pregrammars and Intersection Types}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {14:1--14:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.14}, URN = {urn:nbn:de:0030-drops-134481}, doi = {10.4230/LIPIcs.CSL.2021.14}, annote = {Keywords: Intersection Types, Pregrammars, Inhabitation} } @InProceedings{colcombet_et_al:LIPIcs.CSL.2021.15, author = {Colcombet, Thomas and Petri\c{s}an, Daniela and Stabile, Riccardo}, title = {{Learning Automata and Transducers: A Categorical Approach}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {15:1--15:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.15}, URN = {urn:nbn:de:0030-drops-134498}, doi = {10.4230/LIPIcs.CSL.2021.15}, annote = {Keywords: Automata, transducer, learning, category} } @InProceedings{conghaile_et_al:LIPIcs.CSL.2021.16, author = {Conghaile, Adam \'{O} and Dawar, Anuj}, title = {{Game Comonads \& Generalised Quantifiers}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {16:1--16:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.16}, URN = {urn:nbn:de:0030-drops-134501}, doi = {10.4230/LIPIcs.CSL.2021.16}, annote = {Keywords: Logic, Finite Model Theory, Game Comonads, Generalised Quantifiers} } @InProceedings{dannert_et_al:LIPIcs.CSL.2021.17, author = {Dannert, Katrin M. and Gr\"{a}del, Erich and Naaf, Matthias and Tannen, Val}, title = {{Semiring Provenance for Fixed-Point Logic}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {17:1--17:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.17}, URN = {urn:nbn:de:0030-drops-134518}, doi = {10.4230/LIPIcs.CSL.2021.17}, annote = {Keywords: Finite Model Theory, Semiring Provenance, Absorptive Semirings, Fixed-Point Logics} } @InProceedings{dawar_et_al:LIPIcs.CSL.2021.18, author = {Dawar, Anuj and Sankaran, Abhisekh}, title = {{Extension Preservation in the Finite and Prefix Classes of First Order Logic}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {18:1--18:13}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.18}, URN = {urn:nbn:de:0030-drops-134520}, doi = {10.4230/LIPIcs.CSL.2021.18}, annote = {Keywords: finite model theory, preservation theorems, extension closed, composition, Datalog, Ehrenfeucht-Fraisse games} } @InProceedings{dinis_et_al:LIPIcs.CSL.2021.19, author = {Dinis, Bruno and Miquey, \'{E}tienne}, title = {{Realizability with Stateful Computations for Nonstandard Analysis}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {19:1--19:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.19}, URN = {urn:nbn:de:0030-drops-134531}, doi = {10.4230/LIPIcs.CSL.2021.19}, annote = {Keywords: realizability, nonstandard analysis, states, glueing, ultrafilters, {\L}o\'{s}' theorem} } @InProceedings{echenim_et_al:LIPIcs.CSL.2021.20, author = {Echenim, Mnacho and Iosif, Radu and Peltier, Nicolas}, title = {{Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Establishment}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {20:1--20:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.20}, URN = {urn:nbn:de:0030-drops-134546}, doi = {10.4230/LIPIcs.CSL.2021.20}, annote = {Keywords: Separation logic, Induction definitions, Inductive theorem proving, Entailments, Complexity} } @InProceedings{forster:LIPIcs.CSL.2021.21, author = {Forster, Yannick}, title = {{Church’s Thesis and Related Axioms in Coq’s Type Theory}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {21:1--21:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.21}, URN = {urn:nbn:de:0030-drops-134552}, doi = {10.4230/LIPIcs.CSL.2021.21}, annote = {Keywords: Church’s thesis, constructive type theory, constructive reverse mathematics, synthetic computability theory, Coq} } @InProceedings{ganer_et_al:LIPIcs.CSL.2021.22, author = {Ga{\ss}ner, Christine and Pauly, Arno and Steinberg, Florian}, title = {{Computing Measure as a Primitive Operation in Real Number Computation}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {22:1--22:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.22}, URN = {urn:nbn:de:0030-drops-134564}, doi = {10.4230/LIPIcs.CSL.2021.22}, annote = {Keywords: BSS-machine, Weihrauch reducibility, integrable function, Lebesgue measure, computable analysis} } @InProceedings{geoffroy_et_al:LIPIcs.CSL.2021.23, author = {Geoffroy, Guillaume and Pistone, Paolo}, title = {{A Partial Metric Semantics of Higher-Order Types and Approximate Program Transformations}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {23:1--23:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.23}, URN = {urn:nbn:de:0030-drops-134578}, doi = {10.4230/LIPIcs.CSL.2021.23}, annote = {Keywords: Simply typed \lambda-calculus, program metrics, approximate program transformations, partial metric spaces} } @InProceedings{guerrieri_et_al:LIPIcs.CSL.2021.24, author = {Guerrieri, Giulio and Heijltjes, Willem B. and Paulus, Joseph W.N.}, title = {{A Deep Quantitative Type System}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {24:1--24:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.24}, URN = {urn:nbn:de:0030-drops-134586}, doi = {10.4230/LIPIcs.CSL.2021.24}, annote = {Keywords: Lambda-calculus, Deep inference, Intersection types, Resource calculus} } @InProceedings{guerrieri_et_al:LIPIcs.CSL.2021.25, author = {Guerrieri, Giulio and Olimpieri, Federico}, title = {{Categorifying Non-Idempotent Intersection Types}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {25:1--25:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.25}, URN = {urn:nbn:de:0030-drops-134592}, doi = {10.4230/LIPIcs.CSL.2021.25}, annote = {Keywords: Linear logic, bang calculus, non-idempotent intersection types, distributors, relational semantics, combinatorial species, symmetric sequences, bicategory, categorification} } @InProceedings{gottlinger_et_al:LIPIcs.CSL.2021.26, author = {G\"{o}ttlinger, Merlin and Schr\"{o}der, Lutz and Pattinson, Dirk}, title = {{The Alternating-Time \mu-Calculus with Disjunctive Explicit Strategies}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {26:1--26:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.26}, URN = {urn:nbn:de:0030-drops-134605}, doi = {10.4230/LIPIcs.CSL.2021.26}, annote = {Keywords: Alternating-time logic, multi-agent systems, coalitional strength} } @InProceedings{hannula_et_al:LIPIcs.CSL.2021.27, author = {Hannula, Miika and Kontinen, Juha and L\"{u}ck, Martin and Virtema, Jonni}, title = {{On the Complexity of Horn and Krom Fragments of Second-Order Boolean Logic}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {27:1--27:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.27}, URN = {urn:nbn:de:0030-drops-134610}, doi = {10.4230/LIPIcs.CSL.2021.27}, annote = {Keywords: quantified Boolean formulae, computational complexity, second-order logic, Horn and Krom fragment} } @InProceedings{dejong_et_al:LIPIcs.CSL.2021.28, author = {de Jong, Tom and Escard\'{o}, Mart{\'\i}n H\"{o}tzel}, title = {{Domain Theory in Constructive and Predicative Univalent Foundations}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {28:1--28:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.28}, URN = {urn:nbn:de:0030-drops-134625}, doi = {10.4230/LIPIcs.CSL.2021.28}, annote = {Keywords: domain theory, constructivity, predicativity, univalent foundations} } @InProceedings{kori_et_al:LIPIcs.CSL.2021.29, author = {Kori, Mayuko and Tsukada, Takeshi and Kobayashi, Naoki}, title = {{A Cyclic Proof System for HFL\underline\mathbb{N}}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {29:1--29:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.29}, URN = {urn:nbn:de:0030-drops-134632}, doi = {10.4230/LIPIcs.CSL.2021.29}, annote = {Keywords: Cyclic proof, higher-order logic, fixed-point logic, sequent calculus} } @InProceedings{dilavore_et_al:LIPIcs.CSL.2021.30, author = {Di Lavore, Elena and Hedges, Jules and Soboci\'{n}ski, Pawe{\l}}, title = {{Compositional Modelling of Network Games}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {30:1--30:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.30}, URN = {urn:nbn:de:0030-drops-134645}, doi = {10.4230/LIPIcs.CSL.2021.30}, annote = {Keywords: game theory, category theory, network games, open games, open graphs, compositionality} } @InProceedings{lichter_et_al:LIPIcs.CSL.2021.31, author = {Lichter, Moritz and Schweitzer, Pascal}, title = {{Canonization for Bounded and Dihedral Color Classes in Choiceless Polynomial Time}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {31:1--31:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.31}, URN = {urn:nbn:de:0030-drops-134650}, doi = {10.4230/LIPIcs.CSL.2021.31}, annote = {Keywords: Choiceless polynomial time, canonization, relational structures, bounded color class size, dihedral groups} } @InProceedings{lopez:LIPIcs.CSL.2021.32, author = {Lopez, Aliaume}, title = {{Preservation Theorems Through the Lens of Topology}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {32:1--32:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.32}, URN = {urn:nbn:de:0030-drops-134660}, doi = {10.4230/LIPIcs.CSL.2021.32}, annote = {Keywords: Preservation theorem, Pre-spectral space, Noetherian space, Spectral space} } @InProceedings{pago:LIPIcs.CSL.2021.33, author = {Pago, Benedikt}, title = {{Choiceless Computation and Symmetry: Limitations of Definability}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {33:1--33:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.33}, URN = {urn:nbn:de:0030-drops-134673}, doi = {10.4230/LIPIcs.CSL.2021.33}, annote = {Keywords: finite model theory, descriptive complexity, choiceless computation, symmetries of combinatorial objects} } @InProceedings{pham_et_al:LIPIcs.CSL.2021.34, author = {Pham, Long and Hoffmann, Jan}, title = {{Typable Fragments of Polynomial Automatic Amortized Resource Analysis}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {34:1--34:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.34}, URN = {urn:nbn:de:0030-drops-134681}, doi = {10.4230/LIPIcs.CSL.2021.34}, annote = {Keywords: Resource consumption, Quantitative analysis, Amortized analysis, Typability} } @InProceedings{pistone_et_al:LIPIcs.CSL.2021.35, author = {Pistone, Paolo and Tranchini, Luca}, title = {{The Yoneda Reduction of Polymorphic Types}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {35:1--35:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.35}, URN = {urn:nbn:de:0030-drops-134696}, doi = {10.4230/LIPIcs.CSL.2021.35}, annote = {Keywords: System F, Type isomorphisms, Yoneda isomorphism, Program equivalence} } @InProceedings{rabinovich_et_al:LIPIcs.CSL.2021.36, author = {Rabinovich, Alexander and Tiferet, Doron}, title = {{Degrees of Ambiguity for Parity Tree Automata}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {36:1--36:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.36}, URN = {urn:nbn:de:0030-drops-134709}, doi = {10.4230/LIPIcs.CSL.2021.36}, annote = {Keywords: automata on infinite trees, degree of ambiguity, omega word automata, parity automata} } @InProceedings{schnoebelen:LIPIcs.CSL.2021.37, author = {Schnoebelen, Philippe}, title = {{On Flat Lossy Channel Machines}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {37:1--37:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.37}, URN = {urn:nbn:de:0030-drops-134712}, doi = {10.4230/LIPIcs.CSL.2021.37}, annote = {Keywords: Infinite state systems, Automated verification, Flat systems, Lossy channels} } @InProceedings{tomita:LIPIcs.CSL.2021.38, author = {Tomita, Haruka}, title = {{Realizability Without Symmetry}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {38:1--38:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.38}, URN = {urn:nbn:de:0030-drops-134729}, doi = {10.4230/LIPIcs.CSL.2021.38}, annote = {Keywords: Realizability, combinatory algebra, closed multicategory, closed category, skew closed category} }