@Proceedings{goranko_et_al:LIPIcs.CSL.2017, title = {{LIPIcs, Volume 82, CSL'17, Complete Volume}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017}, URN = {urn:nbn:de:0030-drops-78103}, doi = {10.4230/LIPIcs.CSL.2017}, annote = {Keywords: Conference Proceedings, Software/Program Verification, Formal Definitions and Theory, Language Constructs and Features, Theory of Computation} } @InProceedings{goranko_et_al:LIPIcs.CSL.2017.0, author = {Goranko, Valentin and Dam, Mads}, title = {{Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {0:i--0:xviii}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.0}, URN = {urn:nbn:de:0030-drops-76671}, doi = {10.4230/LIPIcs.CSL.2017.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers} } @InProceedings{dawar_et_al:LIPIcs.CSL.2017.1, author = {Dawar, Anuj and Leivant, Daniel}, title = {{The Ackermann Award 2017}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {1:1--1:4}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.1}, URN = {urn:nbn:de:0030-drops-76938}, doi = {10.4230/LIPIcs.CSL.2017.1}, annote = {Keywords: Ackermann Award, jury report, citation} } @InProceedings{kolaitis:LIPIcs.CSL.2017.2, author = {Kolaitis, Phokion G.}, title = {{Schema Mappings: Structural Properties and Limits}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {2:1--2:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.2}, URN = {urn:nbn:de:0030-drops-76707}, doi = {10.4230/LIPIcs.CSL.2017.2}, annote = {Keywords: logic and databases, schema mappings, data exchange, metric spaces} } @InProceedings{kovacs:LIPIcs.CSL.2017.3, author = {Kov\'{a}cs, Laura}, title = {{First-Order Interpolation and Grey Areas of Proofs}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {3:1--3:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.3}, URN = {urn:nbn:de:0030-drops-76912}, doi = {10.4230/LIPIcs.CSL.2017.3}, annote = {Keywords: theorem proving, interpolation, proof transformations, constraint solving, program analysis} } @InProceedings{kreutzer:LIPIcs.CSL.2017.4, author = {Kreutzer, Stephan}, title = {{Current Trends and New Perspectives for First-Order Model Checking}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {4:1--4:5}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.4}, URN = {urn:nbn:de:0030-drops-77095}, doi = {10.4230/LIPIcs.CSL.2017.4}, annote = {Keywords: Finite Model Theory, Computational Model Theory, Algorithmic Meta Theorems, Model-Checking, Logical Approaches in Graph Theory} } @InProceedings{mahajan:LIPIcs.CSL.2017.5, author = {Mahajan, Meena}, title = {{Arithmetic Circuits: An Overview}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {5:1--5:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.5}, URN = {urn:nbn:de:0030-drops-76858}, doi = {10.4230/LIPIcs.CSL.2017.5}, annote = {Keywords: algebraic complexity, circuits, formulas, branching programs, determinant, permanent} } @InProceedings{thomas:LIPIcs.CSL.2017.6, author = {Thomas, Wolfgang}, title = {{Determinacy of Infinite Games: Perspectives of the Algorithmic Approach}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {6:1--6:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.6}, URN = {urn:nbn:de:0030-drops-77083}, doi = {10.4230/LIPIcs.CSL.2017.6}, annote = {Keywords: Infinite games, descriptive set theory, automata theory, transducers, automatic synthesis} } @InProceedings{veanes:LIPIcs.CSL.2017.7, author = {Veanes, Margus}, title = {{Symbolic Automata Theory with Applications}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {7:1--7:3}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.7}, URN = {urn:nbn:de:0030-drops-76872}, doi = {10.4230/LIPIcs.CSL.2017.7}, annote = {Keywords: automaton, transducer, symbolic} } @InProceedings{ahrens_et_al:LIPIcs.CSL.2017.8, author = {Ahrens, Benedikt and Lumsdaine, Peter LeFanu and Voevodsky, Vladimir}, title = {{Categorical Structures for Type Theory in Univalent Foundations}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {8:1--8:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.8}, URN = {urn:nbn:de:0030-drops-76960}, doi = {10.4230/LIPIcs.CSL.2017.8}, annote = {Keywords: Categorical Semantics, Type Theory, Univalence Axiom} } @InProceedings{alertubella_et_al:LIPIcs.CSL.2017.9, author = {Aler Tubella, Andrea and Guglielmi, Alessio and Ralph, Benjamin}, title = {{Removing Cycles from Proofs}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {9:1--9:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.9}, URN = {urn:nbn:de:0030-drops-77008}, doi = {10.4230/LIPIcs.CSL.2017.9}, annote = {Keywords: proof theory, deep inference, proof complexity} } @InProceedings{angluin_et_al:LIPIcs.CSL.2017.10, author = {Angluin, Dana and Antonopoulos, Timos and Fisman, Dana}, title = {{Query Learning of Derived Omega-Tree Languages in Polynomial Time}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {10:1--10:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.10}, URN = {urn:nbn:de:0030-drops-77022}, doi = {10.4230/LIPIcs.CSL.2017.10}, annote = {Keywords: Learning, queries, infinite trees, derived tree languages, reactive systems} } @InProceedings{bednarczyk_et_al:LIPIcs.CSL.2017.11, author = {Bednarczyk, Bartosz and Charatonik, Witold and Kieronski, Emanuel}, title = {{Extending Two-Variable Logic on Trees}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {11:1--11:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.11}, URN = {urn:nbn:de:0030-drops-76794}, doi = {10.4230/LIPIcs.CSL.2017.11}, annote = {Keywords: two-variable logic, trees, satisfiability, expressivity, counting quantifiers} } @InProceedings{boker:LIPIcs.CSL.2017.12, author = {Boker, Udi}, title = {{On the (In)Succinctness of Muller Automata}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {12:1--12:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.12}, URN = {urn:nbn:de:0030-drops-76751}, doi = {10.4230/LIPIcs.CSL.2017.12}, annote = {Keywords: Automata, Omega-regular languages, Determinization} } @InProceedings{borlido_et_al:LIPIcs.CSL.2017.13, author = {Borlido, C\'{e}lia and Czarnetzki, Silke and Gehrke, Mai and Krebs, Andreas}, title = {{Stone Duality and the Substitution Principle}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {13:1--13:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.13}, URN = {urn:nbn:de:0030-drops-77060}, doi = {10.4230/LIPIcs.CSL.2017.13}, annote = {Keywords: C-variety of languages, typed monoid, Boolean space with an internal monoid, substitution principle, semidirect product} } @InProceedings{boudou_et_al:LIPIcs.CSL.2017.14, author = {Boudou, Joseph and Di\'{e}guez, Mart{\'\i}n and Fern\'{a}ndez-Duque, David}, title = {{A Decidable Intuitionistic Temporal Logic}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {14:1--14:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.14}, URN = {urn:nbn:de:0030-drops-77016}, doi = {10.4230/LIPIcs.CSL.2017.14}, annote = {Keywords: intuitionistic logic, temporal logic, products of modal logics} } @InProceedings{boudou:LIPIcs.CSL.2017.15, author = {Boudou, Joseph}, title = {{Decidable Logics with Associative Binary Modalities}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {15:1--15:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.15}, URN = {urn:nbn:de:0030-drops-76863}, doi = {10.4230/LIPIcs.CSL.2017.15}, annote = {Keywords: modal logics, abstract separation logics, team semantics, resource logics, substructural logics} } @InProceedings{debrecht_et_al:LIPIcs.CSL.2017.16, author = {de Brecht, Matthew and Pauly, Arno}, title = {{Noetherian Quasi-Polish spaces}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {16:1--16:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.16}, URN = {urn:nbn:de:0030-drops-76988}, doi = {10.4230/LIPIcs.CSL.2017.16}, annote = {Keywords: Descriptive set theory, synthetic topology, well-quasi orders, Noetherian spaces, compactness} } @InProceedings{bresolin_et_al:LIPIcs.CSL.2017.17, author = {Bresolin, Davide and Mu\~{n}oz-Velasco, Emilio and Sciavicco, Guido}, title = {{Fast(er) Reasoning in Interval Temporal Logic}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {17:1--17:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.17}, URN = {urn:nbn:de:0030-drops-76782}, doi = {10.4230/LIPIcs.CSL.2017.17}, annote = {Keywords: Temporal Logic, Horn Fragments, Satisfiability, Complexity} } @InProceedings{chatterjee_et_al:LIPIcs.CSL.2017.18, author = {Chatterjee, Krishnendu and Dvor\'{a}k, Wolfgang and Henzinger, Monika and Loitzenbauer, Veronika}, title = {{Improved Set-Based Symbolic Algorithms for Parity Games}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {18:1--18:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.18}, URN = {urn:nbn:de:0030-drops-76830}, doi = {10.4230/LIPIcs.CSL.2017.18}, annote = {Keywords: model checking, graph games, parity games, symbolic computation, progress measure} } @InProceedings{chen_et_al:LIPIcs.CSL.2017.19, author = {Chen, Yijia and Flum, J\"{o}rg and Huang, Xuangui}, title = {{Slicewise Definability in First-Order Logic with Bounded Quantifier Rank}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {19:1--19:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.19}, URN = {urn:nbn:de:0030-drops-76742}, doi = {10.4230/LIPIcs.CSL.2017.19}, annote = {Keywords: first-order logic, quantifier rank, parameterized AC^0, circuit depth} } @InProceedings{cockett_et_al:LIPIcs.CSL.2017.20, author = {Cockett, Robin and Lemay, Jean-Simon}, title = {{Integral Categories and Calculus Categories}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {20:1--20:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.20}, URN = {urn:nbn:de:0030-drops-76687}, doi = {10.4230/LIPIcs.CSL.2017.20}, annote = {Keywords: Differential Categories, Integral Categories, Calculus Categories} } @InProceedings{escardo_et_al:LIPIcs.CSL.2017.21, author = {Escard\'{o}, Mart{\'\i}n H. and Knapp, Cory M.}, title = {{Partial Elements and Recursion via Dominances in Univalent Type Theory}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {21:1--21:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.21}, URN = {urn:nbn:de:0030-drops-76822}, doi = {10.4230/LIPIcs.CSL.2017.21}, annote = {Keywords: univalent type theory, homotopy type theory, partial function, dominance, recursion theory, computability theory} } @InProceedings{carton_et_al:LIPIcs.CSL.2017.22, author = {Carton, Olivier and Finkel, Olivier and Lecomte, Dominique}, title = {{Polishness of Some Topologies Related to Automata}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {22:1--22:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.22}, URN = {urn:nbn:de:0030-drops-76728}, doi = {10.4230/LIPIcs.CSL.2017.22}, annote = {Keywords: Automata and formal languages; logic in computer science; infinite words; B\"{u}chi automaton; regular omega-language; Cantor space; finer topologies; B\"{u}c} } @InProceedings{gerard_et_al:LIPIcs.CSL.2017.23, author = {G\'{e}rard, Ulysse and Miller, Dale}, title = {{Separating Functional Computation from Relations}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {23:1--23:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.23}, URN = {urn:nbn:de:0030-drops-77040}, doi = {10.4230/LIPIcs.CSL.2017.23}, annote = {Keywords: focused proof systems, fixed points, computation and deduction} } @InProceedings{ghica_et_al:LIPIcs.CSL.2017.24, author = {Ghica, Dan R. and Jung, Achim and Lopez, Aliaume}, title = {{Diagrammatic Semantics for Digital Circuits}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {24:1--24:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.24}, URN = {urn:nbn:de:0030-drops-76715}, doi = {10.4230/LIPIcs.CSL.2017.24}, annote = {Keywords: digital circuits, monoidal categories, string diagrams, rewriting, operational semantics} } @InProceedings{fokkink_et_al:LIPIcs.CSL.2017.25, author = {Fokkink, Wan and van Glabbeek, Rob J.}, title = {{Precongruence Formats with Lookahead through Modal Decomposition}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {25:1--25:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.25}, URN = {urn:nbn:de:0030-drops-76776}, doi = {10.4230/LIPIcs.CSL.2017.25}, annote = {Keywords: Structural Operational Semantics, Compositionality, Congruence, Modal Logic, Modal Decomposition, Lookahead} } @InProceedings{gruien:LIPIcs.CSL.2017.26, author = {Gru{\ss}ien, Berit}, title = {{Capturing Logarithmic Space and Polynomial Time on Chordal Claw-Free Graphs}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {26:1--26:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.26}, URN = {urn:nbn:de:0030-drops-76900}, doi = {10.4230/LIPIcs.CSL.2017.26}, annote = {Keywords: Descriptive complexity, logarithmic space, polynomial time, chordal claw-free graphs} } @InProceedings{gradel_et_al:LIPIcs.CSL.2017.27, author = {Gr\"{a}del, Erich and Pago, Benedikt and Pakusa, Wied}, title = {{The Model-Theoretic Expressiveness of Propositional Proof Systems}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {27:1--27:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.27}, URN = {urn:nbn:de:0030-drops-76897}, doi = {10.4230/LIPIcs.CSL.2017.27}, annote = {Keywords: Propositional proof systems, fixed-point logics, resolution, polynomial calculus, generalized quantifiers} } @InProceedings{hannula:LIPIcs.CSL.2017.28, author = {Hannula, Miika}, title = {{Validity and Entailment in Modal and Propositional Dependence Logics}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {28:1--28:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.28}, URN = {urn:nbn:de:0030-drops-76691}, doi = {10.4230/LIPIcs.CSL.2017.28}, annote = {Keywords: modal logic, propositional logic, dependence logic, entailment, validity, complexity} } @InProceedings{vanheerdt_et_al:LIPIcs.CSL.2017.29, author = {van Heerdt, Gerco and Sammartino, Matteo and Silva, Alexandra}, title = {{CALF: Categorical Automata Learning Framework}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {29:1--29:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.29}, URN = {urn:nbn:de:0030-drops-76950}, doi = {10.4230/LIPIcs.CSL.2017.29}, annote = {Keywords: automata learning, category theory} } @InProceedings{klin_et_al:LIPIcs.CSL.2017.30, author = {Klin, Bartek and Lelyk, Mateusz}, title = {{Modal mu-Calculus with Atoms}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {30:1--30:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.30}, URN = {urn:nbn:de:0030-drops-76991}, doi = {10.4230/LIPIcs.CSL.2017.30}, annote = {Keywords: modal mu-calculus, sets with atoms} } @InProceedings{luck:LIPIcs.CSL.2017.31, author = {L\"{u}ck, Martin}, title = {{The Power of the Filtration Technique for Modal Logics with Team Semantics}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {31:1--31:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.31}, URN = {urn:nbn:de:0030-drops-76739}, doi = {10.4230/LIPIcs.CSL.2017.31}, annote = {Keywords: dependence logic,team logic,modal logic,finite model theory} } @InProceedings{muroya_et_al:LIPIcs.CSL.2017.32, author = {Muroya, Koko and Ghica, Dan R.}, title = {{The Dynamic Geometry of Interaction Machine: A Call-by-Need Graph Rewriter}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {32:1--32:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.32}, URN = {urn:nbn:de:0030-drops-76886}, doi = {10.4230/LIPIcs.CSL.2017.32}, annote = {Keywords: Geometry of Interaction, cost analysis, call-by-need reduction} } @InProceedings{deoliveiraoliveira:LIPIcs.CSL.2017.33, author = {de Oliveira Oliveira, Mateus}, title = {{On Supergraphs Satisfying CMSO Properties}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {33:1--33:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.33}, URN = {urn:nbn:de:0030-drops-77058}, doi = {10.4230/LIPIcs.CSL.2017.33}, annote = {Keywords: On Supergraphs Satisfying CMSO Properties} } @InProceedings{pavaux:LIPIcs.CSL.2017.34, author = {Pavaux, Alice}, title = {{Inductive and Functional Types in Ludics}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {34:1--34:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.34}, URN = {urn:nbn:de:0030-drops-77035}, doi = {10.4230/LIPIcs.CSL.2017.34}, annote = {Keywords: Ludics, Inductive types, Fixed point, Linear logic, Game semantics} } @InProceedings{abuzaid_et_al:LIPIcs.CSL.2017.35, author = {Abu Zaid, Faried and Gr\"{a}del, Erich and Reinhardt, Frederic}, title = {{Advice Automatic Structures and Uniformly Automatic Classes}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {35:1--35:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.35}, URN = {urn:nbn:de:0030-drops-76971}, doi = {10.4230/LIPIcs.CSL.2017.35}, annote = {Keywords: automatic structures, algorithmic model theory, decidable theories, torsion-free abelian groups, first-order logic} } @InProceedings{ricciotti_et_al:LIPIcs.CSL.2017.36, author = {Ricciotti, Wilmer and Cheney, James}, title = {{Strongly Normalizing Audited Computation}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {36:1--36:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.36}, URN = {urn:nbn:de:0030-drops-76817}, doi = {10.4230/LIPIcs.CSL.2017.36}, annote = {Keywords: lambda calculus, justification logic, strong normalization, audited computation} } @InProceedings{sankaran:LIPIcs.CSL.2017.37, author = {Sankaran, Abhisekh}, title = {{A Finitary Analogue of the Downward L\"{o}wenheim-Skolem Property}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {37:1--37:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.37}, URN = {urn:nbn:de:0030-drops-77074}, doi = {10.4230/LIPIcs.CSL.2017.37}, annote = {Keywords: downward Lowenheim-Skolem theorem, trees, nested words, tree-depth, cographs, tree representation, translation schemes, composition lemma, f.p.t., log} } @InProceedings{gouveia_et_al:LIPIcs.CSL.2017.38, author = {Gouveia, Maria Jo\~{a}o and Santocanale, Luigi}, title = {{Aleph1 and the Modal mu-Calculus}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {38:1--38:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.38}, URN = {urn:nbn:de:0030-drops-76926}, doi = {10.4230/LIPIcs.CSL.2017.38}, annote = {Keywords: Modal mu-calculus, regular cardinal, continuous function, aleph1, omega1, closure ordinal, ordinal sum} } @InProceedings{vaux:LIPIcs.CSL.2017.39, author = {Vaux, Lionel}, title = {{Taylor Expansion, lambda-Reduction and Normalization}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {39:1--39:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.39}, URN = {urn:nbn:de:0030-drops-76948}, doi = {10.4230/LIPIcs.CSL.2017.39}, annote = {Keywords: lambda-calculus, non-determinism, normalization, denotational semantics} } @InProceedings{verbitsky_et_al:LIPIcs.CSL.2017.40, author = {Verbitsky, Oleg and Zhukovskii, Maksim}, title = {{On the First-Order Complexity of Induced Subgraph Isomorphism}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {40:1--40:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.40}, URN = {urn:nbn:de:0030-drops-76841}, doi = {10.4230/LIPIcs.CSL.2017.40}, annote = {Keywords: the induced subgraph isomorphism problem, descriptive and computational complexity, finite-variable first-order logic, quantifier depth and variable w} } @InProceedings{devisme_et_al:LIPIcs.CSL.2017.41, author = {de Visme, Marc and Winskel, Glynn}, title = {{Strategies with Parallel Causes}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {41:1--41:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.41}, URN = {urn:nbn:de:0030-drops-76800}, doi = {10.4230/LIPIcs.CSL.2017.41}, annote = {Keywords: Games, Strategies, Event Structures, Parallel Causes, Probability} } @InProceedings{horcik_et_al:LIPIcs.CSL.2017.42, author = {Horc{\'\i}k, Rostislav and Moraschini, Tommaso and Vidal, Amanda}, title = {{An Algebraic Approach to Valued Constraint Satisfaction}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {42:1--42:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.42}, URN = {urn:nbn:de:0030-drops-76767}, doi = {10.4230/LIPIcs.CSL.2017.42}, annote = {Keywords: Valued CSP, Polymorphism, pp-definability, Geiger’s Theorem.} }