@Proceedings{talbot_et_al:LIPIcs.CSL.2016, title = {{LIPIcs, Volume 62, CSL'16, Complete Volume}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016}, URN = {urn:nbn:de:0030-drops-66715}, doi = {10.4230/LIPIcs.CSL.2016}, annote = {Keywords: Conference Proceedings, Distributed Systems, Software/ Programs Verifications, Formal Definitions and Theory, Languages Constructs and Features, Knowledge Representations Formalisms and Methods, Theory of Computation, Mathematical Logic} } @InProceedings{talbot_et_al:LIPIcs.CSL.2016.0, author = {Talbot, Jean-Marc and Regnier, Laurent}, title = {{Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {0:i--0:xvi}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.0}, URN = {urn:nbn:de:0030-drops-65405}, doi = {10.4230/LIPIcs.CSL.2016.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers} } @InProceedings{coquand_et_al:LIPIcs.CSL.2016.1, author = {Coquand, Thierry and Dawar, Anuj}, title = {{The Ackermann Award 2016}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {1:1--1:4}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.1}, URN = {urn:nbn:de:0030-drops-65419}, doi = {10.4230/LIPIcs.CSL.2016.1}, annote = {Keywords: Ackermann Award, Computer Science, Logic} } @InProceedings{barto:LIPIcs.CSL.2016.2, author = {Barto, Libor}, title = {{Infinite Domain Constraint Satisfaction Problem}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {2:1--2:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.2}, URN = {urn:nbn:de:0030-drops-65427}, doi = {10.4230/LIPIcs.CSL.2016.2}, annote = {Keywords: Descriptive complexity, Constraint Satisfaction Problem} } @InProceedings{muscholl:LIPIcs.CSL.2016.3, author = {Muscholl, Anca}, title = {{Automated Synthesis: Going Distributed}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {3:1--3:2}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.3}, URN = {urn:nbn:de:0030-drops-65436}, doi = {10.4230/LIPIcs.CSL.2016.3}, annote = {Keywords: Concurrent programs, Distributed synthesis, Runtime monitoring} } @InProceedings{ciabattoni:LIPIcs.CSL.2016.4, author = {Ciabattoni, Agata}, title = {{Analytic Calculi for Non-Classical Logics: Theory and Applications}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {4:1--4:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.4}, URN = {urn:nbn:de:0030-drops-65440}, doi = {10.4230/LIPIcs.CSL.2016.4}, annote = {Keywords: Proof theory, Fuzzy logic} } @InProceedings{silva:LIPIcs.CSL.2016.5, author = {Silva, Alexandra}, title = {{Coalgebraic Learning}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {5:1--5:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.5}, URN = {urn:nbn:de:0030-drops-65455}, doi = {10.4230/LIPIcs.CSL.2016.5}, annote = {Keywords: Automata learning, coalgebraic techniques} } @InProceedings{leiss:LIPIcs.CSL.2016.6, author = {Leiss, Hans}, title = {{The Matrix Ring of a mu-Continuous Chomsky Algebra is mu-Continuous}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {6:1--6:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.6}, URN = {urn:nbn:de:0030-drops-65467}, doi = {10.4230/LIPIcs.CSL.2016.6}, annote = {Keywords: context-free language, fixed point operator, idempotent semiring, matrix ring, Chomsky algebra} } @InProceedings{enqvist_et_al:LIPIcs.CSL.2016.7, author = {Enqvist, Sebastian and Seifan, Fatemeh and Venema, Yde}, title = {{Completeness for Coalgebraic Fixpoint Logic}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {7:1--7:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.7}, URN = {urn:nbn:de:0030-drops-65470}, doi = {10.4230/LIPIcs.CSL.2016.7}, annote = {Keywords: mu-calculus, coalgebra, coalgebraic modal logic, automata, completeness} } @InProceedings{yamada_et_al:LIPIcs.CSL.2016.8, author = {Yamada, Akihisa and Sternagel, Christian and Thiemann, Ren\'{e} and Kusakari, Keiichirou}, title = {{AC Dependency Pairs Revisited}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {8:1--8:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.8}, URN = {urn:nbn:de:0030-drops-65488}, doi = {10.4230/LIPIcs.CSL.2016.8}, annote = {Keywords: Equational Rewriting, Termination, Dependency Pairs, Certification} } @InProceedings{dubut_et_al:LIPIcs.CSL.2016.9, author = {Dubut, J\'{e}r\'{e}my and Goubault, Eric and Goubault-Larrecq, Jean}, title = {{The Directed Homotopy Hypothesis}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {9:1--9:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.9}, URN = {urn:nbn:de:0030-drops-65492}, doi = {10.4230/LIPIcs.CSL.2016.9}, annote = {Keywords: directed algebraic topology, partially enriched categories, homotopy hypothesis, geometric models for concurrency, higher category theory} } @InProceedings{tabuada_et_al:LIPIcs.CSL.2016.10, author = {Tabuada, Paulo and Neider, Daniel}, title = {{Robust Linear Temporal Logic}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {10:1--10:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.10}, URN = {urn:nbn:de:0030-drops-65508}, doi = {10.4230/LIPIcs.CSL.2016.10}, annote = {Keywords: Linear Temporal Logic, Robustness} } @InProceedings{parys_et_al:LIPIcs.CSL.2016.11, author = {Parys, Pawel and Torunczyk, Szymon}, title = {{Models of Lambda-Calculus and the Weak MSO Logic}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {11:1--11:12}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.11}, URN = {urn:nbn:de:0030-drops-65511}, doi = {10.4230/LIPIcs.CSL.2016.11}, annote = {Keywords: typed lambda-calculus, models, weak MSO logic} } @InProceedings{ganardi_et_al:LIPIcs.CSL.2016.12, author = {Ganardi, Moses and G\"{o}ller, Stefan and Lohrey, Markus}, title = {{On the Parallel Complexity of Bisimulation on Finite Systems}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {12:1--12:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.12}, URN = {urn:nbn:de:0030-drops-65522}, doi = {10.4230/LIPIcs.CSL.2016.12}, annote = {Keywords: bisimulation, computational complexity, tree width} } @InProceedings{kotek_et_al:LIPIcs.CSL.2016.13, author = {Kotek, Tomer and Veith, Helmut and Zuleger, Florian}, title = {{Monadic Second Order Finite Satisfiability and Unbounded Tree-Width}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {13:1--13:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.13}, URN = {urn:nbn:de:0030-drops-65537}, doi = {10.4230/LIPIcs.CSL.2016.13}, annote = {Keywords: Monadic Second Order Logic MSO, Two variable Fragment with Counting C2, Finite decidability, Unbounded Tree-width, WS1S with Cardinality Constraints} } @InProceedings{hella_et_al:LIPIcs.CSL.2016.14, author = {Hella, Lauri and Kolaitis, Phokion G.}, title = {{Dependence Logic vs. Constraint Satisfaction}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {14:1--14:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.14}, URN = {urn:nbn:de:0030-drops-65548}, doi = {10.4230/LIPIcs.CSL.2016.14}, annote = {Keywords: Dependence logic, constraint satisfaction, computational complexity, expressive power} } @InProceedings{chen_et_al:LIPIcs.CSL.2016.15, author = {Chen, Hubie and Mayr, Peter}, title = {{Quantified Constraint Satisfaction on Monoids}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {15:1--15:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.15}, URN = {urn:nbn:de:0030-drops-65553}, doi = {10.4230/LIPIcs.CSL.2016.15}, annote = {Keywords: quantified constraint satisfaction, universal algebra, computational complexity} } @InProceedings{atserias_et_al:LIPIcs.CSL.2016.16, author = {Atserias, Albert and Torunczyk, Szymon}, title = {{Non-Homogenizable Classes of Finite Structures}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {16:1--16:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.16}, URN = {urn:nbn:de:0030-drops-65563}, doi = {10.4230/LIPIcs.CSL.2016.16}, annote = {Keywords: Fra\"{i}ss\'{e} class, amalgmation class, reduct, Constraint Satisfaction Problem, bounded width} } @InProceedings{elberfeld:LIPIcs.CSL.2016.17, author = {Elberfeld, Michael}, title = {{Context-Free Graph Properties via Definable Decompositions}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {17:1--17:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.17}, URN = {urn:nbn:de:0030-drops-65575}, doi = {10.4230/LIPIcs.CSL.2016.17}, annote = {Keywords: finite model theory, monadic second-order logic, tree decomposition, context-free languages, expressive power} } @InProceedings{eickmeyer_et_al:LIPIcs.CSL.2016.18, author = {Eickmeyer, Kord and Kawarabayashi, Ken-ichi}, title = {{Successor-Invariant First-Order Logic on Graphs with Excluded Topological Subgraphs}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {18:1--18:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.18}, URN = {urn:nbn:de:0030-drops-65583}, doi = {10.4230/LIPIcs.CSL.2016.18}, annote = {Keywords: model-checking, algorithmic meta-theorem, successor-invariant, first-order logic, topological subgraphs, parameterised complexity} } @InProceedings{pakusa_et_al:LIPIcs.CSL.2016.19, author = {Pakusa, Wied and Schalth\"{o}fer, Svenja and Selman, Erkal}, title = {{Definability of Cai-F\"{u}rer-Immerman Problems in Choiceless Polynomial Time}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {19:1--19:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.19}, URN = {urn:nbn:de:0030-drops-65595}, doi = {10.4230/LIPIcs.CSL.2016.19}, annote = {Keywords: finite model theory, descriptive complexity, logic for textsc\{Ptime\}, Choiceless Polynomial Time, Cai-F\"{u}rer-Immerman} } @InProceedings{durand_et_al:LIPIcs.CSL.2016.20, author = {Durand, Arnaud and Haak, Anselm and Kontinen, Juha and Vollmer, Heribert}, title = {{Descriptive Complexity of #AC^0 Functions}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {20:1--20:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.20}, URN = {urn:nbn:de:0030-drops-65601}, doi = {10.4230/LIPIcs.CSL.2016.20}, annote = {Keywords: finite model theory, Fagin's theorem, arithmetic circuits, counting classes, Skolem function} } @InProceedings{altenkirch_et_al:LIPIcs.CSL.2016.21, author = {Altenkirch, Thorsten and Capriotti, Paolo and Kraus, Nicolai}, title = {{Extending Homotopy Type Theory with Strict Equality}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {21:1--21:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.21}, URN = {urn:nbn:de:0030-drops-65612}, doi = {10.4230/LIPIcs.CSL.2016.21}, annote = {Keywords: homotopy type theory, coherences, strict equality, homotopy type system} } @InProceedings{hou(favonia)_et_al:LIPIcs.CSL.2016.22, author = {Hou (Favonia), Kuen-Bang and Shulman, Michael}, title = {{The Seifert-van Kampen Theorem in Homotopy Type Theory}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {22:1--22:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.22}, URN = {urn:nbn:de:0030-drops-65626}, doi = {10.4230/LIPIcs.CSL.2016.22}, annote = {Keywords: homotopy type theory, fundamental group, homotopy pushout, mechanized reasoning} } @InProceedings{birkedal_et_al:LIPIcs.CSL.2016.23, author = {Birkedal, Lars and Bizjak, Ale\v{s} and Clouston, Ranald and Grathwohl, Hans Bugge and Spitters, Bas and Vezzosi, Andrea}, title = {{Guarded Cubical Type Theory: Path Equality for Guarded Recursion}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {23:1--23:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.23}, URN = {urn:nbn:de:0030-drops-65638}, doi = {10.4230/LIPIcs.CSL.2016.23}, annote = {Keywords: Guarded Recursion, Dependent Type Theory, Cubical Type Theory, Denotational Semantics, Homotopy Type Theory} } @InProceedings{orton_et_al:LIPIcs.CSL.2016.24, author = {Orton, Ian and Pitts, Andrew M.}, title = {{Axioms for Modelling Cubical Type Theory in a Topos}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {24:1--24:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.24}, URN = {urn:nbn:de:0030-drops-65647}, doi = {10.4230/LIPIcs.CSL.2016.24}, annote = {Keywords: models of dependent type theory, homotopy type theory, cubical sets, cubical type theory, topos, univalence} } @InProceedings{krivine:LIPIcs.CSL.2016.25, author = {Krivine, Jean-Louis}, title = {{Bar Recursion in Classical Realisability: Dependent Choice and Continuum Hypothesis}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {25:1--25:11}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.25}, URN = {urn:nbn:de:0030-drops-65650}, doi = {10.4230/LIPIcs.CSL.2016.25}, annote = {Keywords: lambda-calculus, Curry-Howard correspondence, set theory} } @InProceedings{berger:LIPIcs.CSL.2016.26, author = {Berger, Ulrich}, title = {{Extracting Non-Deterministic Concurrent Programs}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {26:1--26:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.26}, URN = {urn:nbn:de:0030-drops-65669}, doi = {10.4230/LIPIcs.CSL.2016.26}, annote = {Keywords: Proof theory, realizability, program extraction, non-determinism, concurrency, computable analysis} } @InProceedings{laird:LIPIcs.CSL.2016.27, author = {Laird, James}, title = {{Polymorphic Game Semantics for Dynamic Binding}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {27:1--27:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.27}, URN = {urn:nbn:de:0030-drops-65671}, doi = {10.4230/LIPIcs.CSL.2016.27}, annote = {Keywords: Game semantics, denotational models, PCF, Idealized Algol} } @InProceedings{almagor_et_al:LIPIcs.CSL.2016.28, author = {Almagor, Shaull and Kupferman, Orna}, title = {{High-Quality Synthesis Against Stochastic Environments}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {28:1--28:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.28}, URN = {urn:nbn:de:0030-drops-65688}, doi = {10.4230/LIPIcs.CSL.2016.28}, annote = {Keywords: Stochastic and Quantitative Synthesis, Markov Decision Process} } @InProceedings{alur_et_al:LIPIcs.CSL.2016.29, author = {Alur, Rajeev and Faella, Marco and Kannan, Sampath and Singhania, Nimit}, title = {{Hedging Bets in Markov Decision Processes}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {29:1--29:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.29}, URN = {urn:nbn:de:0030-drops-65698}, doi = {10.4230/LIPIcs.CSL.2016.29}, annote = {Keywords: Markov decision processes, Infinite state systems, Multi-objective optimization} } @InProceedings{hunter_et_al:LIPIcs.CSL.2016.30, author = {Hunter, Paul and P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, title = {{Minimizing Regret in Discounted-Sum Games}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {30:1--30:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.30}, URN = {urn:nbn:de:0030-drops-65704}, doi = {10.4230/LIPIcs.CSL.2016.30}, annote = {Keywords: Quantitative games, Regret, Verification, Synthesis, Game theory} } @InProceedings{weinert_et_al:LIPIcs.CSL.2016.31, author = {Weinert, Alexander and Zimmermann, Martin}, title = {{Easy to Win, Hard to Master: Optimal Strategies in Parity Games with Costs}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {31:1--31:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.31}, URN = {urn:nbn:de:0030-drops-65714}, doi = {10.4230/LIPIcs.CSL.2016.31}, annote = {Keywords: Parity Games with Costs, Optimal Strategies, Memory Requirements, Tradeoffs} } @InProceedings{baelde_et_al:LIPIcs.CSL.2016.32, author = {Baelde, David and Lunel, Simon and Schmitz, Sylvain}, title = {{A Sequent Calculus for a Modal Logic on Finite Data Trees}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {32:1--32:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.32}, URN = {urn:nbn:de:0030-drops-65720}, doi = {10.4230/LIPIcs.CSL.2016.32}, annote = {Keywords: XPath, proof systems, modal logic, complexity} } @InProceedings{luck:LIPIcs.CSL.2016.33, author = {L\"{u}ck, Martin}, title = {{Axiomatizations for Propositional and Modal Team Logic}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {33:1--33:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.33}, URN = {urn:nbn:de:0030-drops-65739}, doi = {10.4230/LIPIcs.CSL.2016.33}, annote = {Keywords: team logic, propositional team logic, modal team logic, proof system, axiomatization} } @InProceedings{bana_et_al:LIPIcs.CSL.2016.34, author = {Bana, Gergei and Okada, Mitsuhiro}, title = {{Semantics for "Enough-Certainty" and Fitting's Embedding of Classical Logic in S4}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {34:1--34:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.34}, URN = {urn:nbn:de:0030-drops-65746}, doi = {10.4230/LIPIcs.CSL.2016.34}, annote = {Keywords: first-order logic, possible-world semantics, Fitting embedding, asymptotic probabilities, verification of complexity-theoretic properties} } @InProceedings{gradel_et_al:LIPIcs.CSL.2016.35, author = {Gr\"{a}del, Erich and Hegselmann, Stefan}, title = {{Counting in Team Semantics}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {35:1--35:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.35}, URN = {urn:nbn:de:0030-drops-65757}, doi = {10.4230/LIPIcs.CSL.2016.35}, annote = {Keywords: logics with counting, team semantics, fixed-point logic with counting} } @InProceedings{kolodziejczyk_et_al:LIPIcs.CSL.2016.36, author = {Kolodziejczyk, Leszek Aleksander and Michalewski, Henryk and Pradic, Pierre and Skrzypczak, Michal}, title = {{The Logical Strength of B\"{u}chi's Decidability Theorem}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {36:1--36:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.36}, URN = {urn:nbn:de:0030-drops-65765}, doi = {10.4230/LIPIcs.CSL.2016.36}, annote = {Keywords: nondeterministic automata, monadic second-order logic, B\"{u}chi's theorem, additive Ramsey's theorem, reverse mathematics} } @InProceedings{karandikar_et_al:LIPIcs.CSL.2016.37, author = {Karandikar, Prateek and Schnoebelen, Philippe}, title = {{The Height of Piecewise-Testable Languages with Applications in Logical Complexity}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {37:1--37:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.37}, URN = {urn:nbn:de:0030-drops-65776}, doi = {10.4230/LIPIcs.CSL.2016.37}, annote = {Keywords: Descriptive complexity} } @InProceedings{kieronski:LIPIcs.CSL.2016.38, author = {Kieronski, Emanuel}, title = {{One-Dimensional Logic over Words}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {38:1--38:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.38}, URN = {urn:nbn:de:0030-drops-65782}, doi = {10.4230/LIPIcs.CSL.2016.38}, annote = {Keywords: satisfiability, expressivity, words, fragments of first-order logic} } @InProceedings{pratthartmann_et_al:LIPIcs.CSL.2016.39, author = {Pratt-Hartmann, Ian and Szwast, Wieslaw and Tendera, Lidia}, title = {{Quine's Fluted Fragment is Non-Elementary}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {39:1--39:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.39}, URN = {urn:nbn:de:0030-drops-65791}, doi = {10.4230/LIPIcs.CSL.2016.39}, annote = {Keywords: Quine, fluted fragment, Purdy, non-elementary, satisfiability, decidability} } @InProceedings{baillot_et_al:LIPIcs.CSL.2016.40, author = {Baillot, Patrick and Das, Anupam}, title = {{Free-Cut Elimination in Linear Logic and an Application to a Feasible Arithmetic}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {40:1--40:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.40}, URN = {urn:nbn:de:0030-drops-65807}, doi = {10.4230/LIPIcs.CSL.2016.40}, annote = {Keywords: proof theory, linear logic, bounded arithmetic, polynomial time computation, implicit computational complexity} } @InProceedings{decarvalho:LIPIcs.CSL.2016.41, author = {de Carvalho, Daniel}, title = {{The Relational Model Is Injective for Multiplicative Exponential Linear Logic}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {41:1--41:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.41}, URN = {urn:nbn:de:0030-drops-65815}, doi = {10.4230/LIPIcs.CSL.2016.41}, annote = {Keywords: Linear Logic, Denotational semantics, Proof-nets} } @InProceedings{baelde_et_al:LIPIcs.CSL.2016.42, author = {Baelde, David and Doumane, Amina and Saurin, Alexis}, title = {{Infinitary Proof Theory: the Multiplicative Additive Case}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {42:1--42:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.42}, URN = {urn:nbn:de:0030-drops-65825}, doi = {10.4230/LIPIcs.CSL.2016.42}, annote = {Keywords: Infinitary proofs, linear logic} }