24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@Proceedings{kreutzer:LIPIcs.CSL.2015, title = {{LIPIcs, Volume 41, CSL'15, Complete Volume}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015}, URN = {urn:nbn:de:0030-drops-54670}, doi = {10.4230/LIPIcs.CSL.2015}, 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} }
24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. i-xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{kreutzer:LIPIcs.CSL.2015.i, author = {Kreutzer, Stephan}, title = {{Front Matter, Table of Contents, Preface, Conference Organisation, External Reviewers}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {i--xiv}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.i}, URN = {urn:nbn:de:0030-drops-54489}, doi = {10.4230/LIPIcs.CSL.2015.i}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organisation, External Reviewers} }
Anuj Dawar, Dexter Kozen, and Simona Ronchi Della Rocca. The Ackermann Award 2015. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 15-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{dawar_et_al:LIPIcs.CSL.2015.xv, author = {Dawar, Anuj and Kozen, Dexter and Ronchi Della Rocca, Simona}, title = {{The Ackermann Award 2015}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {15--18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.xv}, URN = {urn:nbn:de:0030-drops-54470}, doi = {10.4230/LIPIcs.CSL.2015.xv}, annote = {Keywords: Ackermann Award} }
Martín Abadi. The Prophecy of Timely Rollback (Invited Talk). In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, p. 1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{abadi:LIPIcs.CSL.2015.1, author = {Abadi, Mart{\'\i}n}, title = {{The Prophecy of Timely Rollback}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {1--1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.1}, URN = {urn:nbn:de:0030-drops-54452}, doi = {10.4230/LIPIcs.CSL.2015.1}, annote = {Keywords: Dataflow, refinement, rollback} }
Claudia Carapelle and Markus Lohrey. Temporal Logics with Local Constraints (Invited Talk). In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 2-13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{carapelle_et_al:LIPIcs.CSL.2015.2, author = {Carapelle, Claudia and Lohrey, Markus}, title = {{Temporal Logics with Local Constraints}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {2--13}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.2}, URN = {urn:nbn:de:0030-drops-54465}, doi = {10.4230/LIPIcs.CSL.2015.2}, annote = {Keywords: Temporal logics with constraints, concrete domains, LTL, CTL*, ECTL*} }
R. Ryan Williams. Thinking Algorithmically About Impossibility (Invited Talk). In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 14-23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{williams:LIPIcs.CSL.2015.14, author = {Williams, R. Ryan}, title = {{Thinking Algorithmically About Impossibility}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {14--23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.14}, URN = {urn:nbn:de:0030-drops-54396}, doi = {10.4230/LIPIcs.CSL.2015.14}, annote = {Keywords: satisfiability, derandomization, circuit complexity} }
Damiano Mazza. Simple Parsimonious Types and Logarithmic Space. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 24-40, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{mazza:LIPIcs.CSL.2015.24, author = {Mazza, Damiano}, title = {{Simple Parsimonious Types and Logarithmic Space}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {24--40}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.24}, URN = {urn:nbn:de:0030-drops-54053}, doi = {10.4230/LIPIcs.CSL.2015.24}, annote = {Keywords: implicit computational complexity, linear logic, geometry of interaction} }
Simone Bova and Barnaby Martin. First-Order Queries on Finite Abelian Groups. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 41-59, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{bova_et_al:LIPIcs.CSL.2015.41, author = {Bova, Simone and Martin, Barnaby}, title = {{First-Order Queries on Finite Abelian Groups}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {41--59}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.41}, URN = {urn:nbn:de:0030-drops-54060}, doi = {10.4230/LIPIcs.CSL.2015.41}, annote = {Keywords: Finite Abelian Groups, First-Order Logic, Monadic Second-Order Logic} }
Anuj Dawar and Pengming Wang. A Definability Dichotomy for Finite Valued CSPs. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 60-77, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{dawar_et_al:LIPIcs.CSL.2015.60, author = {Dawar, Anuj and Wang, Pengming}, title = {{A Definability Dichotomy for Finite Valued CSPs}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {60--77}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.60}, URN = {urn:nbn:de:0030-drops-54078}, doi = {10.4230/LIPIcs.CSL.2015.60}, annote = {Keywords: descriptive complexity, constraint satisfaction, definability, fixed-point logic, optimization} }
Sjoerd Cranen, Bas Luttik, and Tim A. C. Willemse. Evidence for Fixpoint Logic. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 78-93, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{cranen_et_al:LIPIcs.CSL.2015.78, author = {Cranen, Sjoerd and Luttik, Bas and Willemse, Tim A. C.}, title = {{Evidence for Fixpoint Logic}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {78--93}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.78}, URN = {urn:nbn:de:0030-drops-54080}, doi = {10.4230/LIPIcs.CSL.2015.78}, annote = {Keywords: fixpoint logic, diagnostics, counterexample, model checking, stuttering bisimilarity, ACTL*} }
Matthias Baaz and Christian G. Fermüller. Elementary Elimination of Prenex Cuts in Disjunction-free Intuitionistic Logic. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 94-109, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{baaz_et_al:LIPIcs.CSL.2015.94, author = {Baaz, Matthias and Ferm\"{u}ller, Christian G.}, title = {{Elementary Elimination of Prenex Cuts in Disjunction-free Intuitionistic Logic}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {94--109}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.94}, URN = {urn:nbn:de:0030-drops-54097}, doi = {10.4230/LIPIcs.CSL.2015.94}, annote = {Keywords: Cut-elimination, sequent calculus, intuitionistic logic} }
Stefan Hetzl and Sebastian Zivota. Tree Grammars for the Elimination of Non-prenex Cuts. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 110-127, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{hetzl_et_al:LIPIcs.CSL.2015.110, author = {Hetzl, Stefan and Zivota, Sebastian}, title = {{Tree Grammars for the Elimination of Non-prenex Cuts}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {110--127}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.110}, URN = {urn:nbn:de:0030-drops-54103}, doi = {10.4230/LIPIcs.CSL.2015.110}, annote = {Keywords: proof theory, cut-elimination, Herbrand's theorem, tree grammars} }
Aleksy Schubert, Wil Dekkers, and Henk P. Barendregt. Automata Theoretic Account of Proof Search. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 128-143, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{schubert_et_al:LIPIcs.CSL.2015.128, author = {Schubert, Aleksy and Dekkers, Wil and Barendregt, Henk P.}, title = {{Automata Theoretic Account of Proof Search}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {128--143}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.128}, URN = {urn:nbn:de:0030-drops-54113}, doi = {10.4230/LIPIcs.CSL.2015.128}, annote = {Keywords: simple types, automata, trees, languages of proofs} }
Filip Mazowiecki and Cristian Riveros. Maximal Partition Logic: Towards a Logical Characterization of Copyless Cost Register Automata. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 144-159, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{mazowiecki_et_al:LIPIcs.CSL.2015.144, author = {Mazowiecki, Filip and Riveros, Cristian}, title = {{Maximal Partition Logic: Towards a Logical Characterization of Copyless Cost Register Automata}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {144--159}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.144}, URN = {urn:nbn:de:0030-drops-54127}, doi = {10.4230/LIPIcs.CSL.2015.144}, annote = {Keywords: MSO, Finite Automata, Cost Register Automata, Weighted Automata, Weighted Logics, Semirings} }
Olivier Carton and Luc Dartois. Aperiodic Two-way Transducers and FO-Transductions. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 160-174, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{carton_et_al:LIPIcs.CSL.2015.160, author = {Carton, Olivier and Dartois, Luc}, title = {{Aperiodic Two-way Transducers and FO-Transductions}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {160--174}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.160}, URN = {urn:nbn:de:0030-drops-54133}, doi = {10.4230/LIPIcs.CSL.2015.160}, annote = {Keywords: Transducer, first-order, two-way, transition monoid, aperiodic} }
Orna Kupferman and Gal Vardi. On Relative and Probabilistic Finite Counterability. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 175-192, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{kupferman_et_al:LIPIcs.CSL.2015.175, author = {Kupferman, Orna and Vardi, Gal}, title = {{On Relative and Probabilistic Finite Counterability}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {175--192}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.175}, URN = {urn:nbn:de:0030-drops-54147}, doi = {10.4230/LIPIcs.CSL.2015.175}, annote = {Keywords: Model Checking, Counterexamples, Safety, Liveness, Probability, omega-Regular Languages} }
Alberto Molinari, Angelo Montanari, and Adriano Peron. A Model Checking Procedure for Interval Temporal Logics based on Track Representatives. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 193-210, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{molinari_et_al:LIPIcs.CSL.2015.193, author = {Molinari, Alberto and Montanari, Angelo and Peron, Adriano}, title = {{A Model Checking Procedure for Interval Temporal Logics based on Track Representatives}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {193--210}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.193}, URN = {urn:nbn:de:0030-drops-54150}, doi = {10.4230/LIPIcs.CSL.2015.193}, annote = {Keywords: Interval Temporal Logic, Model Checking, Complexity} }
Samson Abramsky, Rui Soares Barbosa, Kohei Kishida, Raymond Lal, and Shane Mansfield. Contextuality, Cohomology and Paradox. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 211-228, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{abramsky_et_al:LIPIcs.CSL.2015.211, author = {Abramsky, Samson and Soares Barbosa, Rui and Kishida, Kohei and Lal, Raymond and Mansfield, Shane}, title = {{Contextuality, Cohomology and Paradox}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {211--228}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.211}, URN = {urn:nbn:de:0030-drops-54166}, doi = {10.4230/LIPIcs.CSL.2015.211}, annote = {Keywords: Quantum mechanics, contextuality, sheaf theory, cohomology, logical paradoxes} }
Sylvain Salvati and Igor Walukiewicz. A Model for Behavioural Properties of Higher-order Programs. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 229-243, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{salvati_et_al:LIPIcs.CSL.2015.229, author = {Salvati, Sylvain and Walukiewicz, Igor}, title = {{A Model for Behavioural Properties of Higher-order Programs}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {229--243}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.229}, URN = {urn:nbn:de:0030-drops-54173}, doi = {10.4230/LIPIcs.CSL.2015.229}, annote = {Keywords: Simply typed lambda-Y-calculus, Monadic second order logic, semantic models} }
Lorenzo Clemente and Slawomir Lasota. Reachability Analysis of First-order Definable Pushdown Systems. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 244-259, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{clemente_et_al:LIPIcs.CSL.2015.244, author = {Clemente, Lorenzo and Lasota, Slawomir}, title = {{Reachability Analysis of First-order Definable Pushdown Systems}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {244--259}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.244}, URN = {urn:nbn:de:0030-drops-54185}, doi = {10.4230/LIPIcs.CSL.2015.244}, annote = {Keywords: automata theory, pushdown systems, sets with atoms, saturation technique} }
Charles Grellois and Paul-André Melliès. Relational Semantics of Linear Logic and Higher-order Model Checking. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 260-276, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{grellois_et_al:LIPIcs.CSL.2015.260, author = {Grellois, Charles and Melli\`{e}s, Paul-Andr\'{e}}, title = {{Relational Semantics of Linear Logic and Higher-order Model Checking}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {260--276}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.260}, URN = {urn:nbn:de:0030-drops-54190}, doi = {10.4230/LIPIcs.CSL.2015.260}, annote = {Keywords: Higher-order model-checking, linear logic, relational semantics, parity games, parametric comonads.} }
Juha Kontinen, Julian-Steffen Müller, Henning Schnoor, and Heribert Vollmer. A Van Benthem Theorem for Modal Team Semantics. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 277-291, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{kontinen_et_al:LIPIcs.CSL.2015.277, author = {Kontinen, Juha and M\"{u}ller, Julian-Steffen and Schnoor, Henning and Vollmer, Heribert}, title = {{A Van Benthem Theorem for Modal Team Semantics}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {277--291}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.277}, URN = {urn:nbn:de:0030-drops-54206}, doi = {10.4230/LIPIcs.CSL.2015.277}, annote = {Keywords: modal logic, dependence logic, team semantics, expressivity, bisimulation, independence, inclusion, generalized dependence atom} }
Katsuhiko Sano and Jonni Virtema. Axiomatizing Propositional Dependence Logics. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 292-307, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{sano_et_al:LIPIcs.CSL.2015.292, author = {Sano, Katsuhiko and Virtema, Jonni}, title = {{Axiomatizing Propositional Dependence Logics}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {292--307}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.292}, URN = {urn:nbn:de:0030-drops-54215}, doi = {10.4230/LIPIcs.CSL.2015.292}, annote = {Keywords: propositional dependence logic, modal dependence logic, axiomatization, tableau calculus} }
Thomas Schwentick, Nils Vortmeier, and Thomas Zeume. Static Analysis for Logic-based Dynamic Programs. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 308-324, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{schwentick_et_al:LIPIcs.CSL.2015.308, author = {Schwentick, Thomas and Vortmeier, Nils and Zeume, Thomas}, title = {{Static Analysis for Logic-based Dynamic Programs}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {308--324}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.308}, URN = {urn:nbn:de:0030-drops-54221}, doi = {10.4230/LIPIcs.CSL.2015.308}, annote = {Keywords: Dynamic descriptive complexity, algorithmic problems, emptiness, history independence, consistency} }
James Brotherston and Jules Villard. Sub-classical Boolean Bunched Logics and the Meaning of Par. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 325-342, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{brotherston_et_al:LIPIcs.CSL.2015.325, author = {Brotherston, James and Villard, Jules}, title = {{Sub-classical Boolean Bunched Logics and the Meaning of Par}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {325--342}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.325}, URN = {urn:nbn:de:0030-drops-54234}, doi = {10.4230/LIPIcs.CSL.2015.325}, annote = {Keywords: Bunched logic, linear logic, modal logic, Kripke semantics, model theory} }
Stefano Berardi. Classical and Intuitionistic Arithmetic with Higher Order Comprehension Coincide on Inductive Well-Foundedness. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 343-358, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{berardi:LIPIcs.CSL.2015.343, author = {Berardi, Stefano}, title = {{Classical and Intuitionistic Arithmetic with Higher Order Comprehension Coincide on Inductive Well-Foundedness}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {343--358}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.343}, URN = {urn:nbn:de:0030-drops-54246}, doi = {10.4230/LIPIcs.CSL.2015.343}, annote = {Keywords: Intuitionism, Inductive Definitions, Proof Theory, impredicativity, omega rule} }
Paolo Capriotti, Nicolai Kraus, and Andrea Vezzosi. Functions out of Higher Truncations. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 359-373, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{capriotti_et_al:LIPIcs.CSL.2015.359, author = {Capriotti, Paolo and Kraus, Nicolai and Vezzosi, Andrea}, title = {{Functions out of Higher Truncations}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {359--373}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.359}, URN = {urn:nbn:de:0030-drops-54257}, doi = {10.4230/LIPIcs.CSL.2015.359}, annote = {Keywords: homotopy type theory, truncation elimination, constancy on loop spaces} }
Murdoch J. Gabbay, Dan R. Ghica, and Daniela Petrisan. Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 374-389, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{gabbay_et_al:LIPIcs.CSL.2015.374, author = {Gabbay, Murdoch J. and Ghica, Dan R. and Petrisan, Daniela}, title = {{Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {374--389}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.374}, URN = {urn:nbn:de:0030-drops-54262}, doi = {10.4230/LIPIcs.CSL.2015.374}, annote = {Keywords: nominal sets, scope, alpha equivalence, dynamic sequences} }
Erich Grädel and Wied Pakusa. Rank Logic is Dead, Long Live Rank Logic!. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 390-404, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{gradel_et_al:LIPIcs.CSL.2015.390, author = {Gr\"{a}del, Erich and Pakusa, Wied}, title = {{Rank Logic is Dead, Long Live Rank Logic!}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {390--404}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.390}, URN = {urn:nbn:de:0030-drops-54279}, doi = {10.4230/LIPIcs.CSL.2015.390}, annote = {Keywords: logic, descriptive complexity, polynomial time, rank logic} }
Adrià Gascón, Manfred Schmidt-Schauß, and Ashish Tiwari. Two-Restricted One Context Unification is in Polynomial Time. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 405-422, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{gascon_et_al:LIPIcs.CSL.2015.405, author = {Gasc\'{o}n, Adri\`{a} and Schmidt-Schau{\ss}, Manfred and Tiwari, Ashish}, title = {{Two-Restricted One Context Unification is in Polynomial Time}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {405--422}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.405}, URN = {urn:nbn:de:0030-drops-54289}, doi = {10.4230/LIPIcs.CSL.2015.405}, annote = {Keywords: context unification, first-order unification, deduction, type checking} }
Jiaxiang Liu, Jean-Pierre Jouannaud, and Mizuhito Ogawa. Confluence of Layered Rewrite Systems. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 423-440, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{liu_et_al:LIPIcs.CSL.2015.423, author = {Liu, Jiaxiang and Jouannaud, Jean-Pierre and Ogawa, Mizuhito}, title = {{Confluence of Layered Rewrite Systems}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {423--440}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.423}, URN = {urn:nbn:de:0030-drops-54293}, doi = {10.4230/LIPIcs.CSL.2015.423}, annote = {Keywords: Layers, confluence, decreasing diagrams, critical pairs, cyclic unification} }
Lukasz Kaiser, Martin Lang, Simon Leßenich, and Christof Löding. A Unified Approach to Boundedness Properties in MSO. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 441-456, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{kaiser_et_al:LIPIcs.CSL.2015.441, author = {Kaiser, Lukasz and Lang, Martin and Le{\ss}enich, Simon and L\"{o}ding, Christof}, title = {{A Unified Approach to Boundedness Properties in MSO}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {441--456}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.441}, URN = {urn:nbn:de:0030-drops-54309}, doi = {10.4230/LIPIcs.CSL.2015.441}, annote = {Keywords: quantitative logics, monadic second order logic, boundedness, automatic structures, tree automata} }
Karoliina Lehtinen and Sandra Quickert. Deciding the First Levels of the Modal mu Alternation Hierarchy by Formula Construction. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 457-471, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{lehtinen_et_al:LIPIcs.CSL.2015.457, author = {Lehtinen, Karoliina and Quickert, Sandra}, title = {{Deciding the First Levels of the Modal mu Alternation Hierarchy by Formula Construction}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {457--471}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.457}, URN = {urn:nbn:de:0030-drops-54316}, doi = {10.4230/LIPIcs.CSL.2015.457}, annote = {Keywords: modal mu calculus, fixpoint logic, alternation hierarchy} }
Dietrich Kuske, Jiamou Liu, and Anastasia Moskvina. Infinite and Bi-infinite Words with Decidable Monadic Theories. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 472-486, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{kuske_et_al:LIPIcs.CSL.2015.472, author = {Kuske, Dietrich and Liu, Jiamou and Moskvina, Anastasia}, title = {{Infinite and Bi-infinite Words with Decidable Monadic Theories}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {472--486}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.472}, URN = {urn:nbn:de:0030-drops-54325}, doi = {10.4230/LIPIcs.CSL.2015.472}, annote = {Keywords: infinite words, bi-infinite words, monadic second order logic} }
Dmitriy Traytel. A Coalgebraic Decision Procedure for WS1S. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 487-503, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{traytel:LIPIcs.CSL.2015.487, author = {Traytel, Dmitriy}, title = {{A Coalgebraic Decision Procedure for WS1S}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {487--503}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.487}, URN = {urn:nbn:de:0030-drops-54335}, doi = {10.4230/LIPIcs.CSL.2015.487}, annote = {Keywords: WS1S, decision procedure, coalgebra, Brzozowski derivatives, Isabelle} }
Thomas Brihaye, Véronique Bruyère, Noémie Meunier, and Jean-Francois Raskin. Weak Subgame Perfect Equilibria and their Application to Quantitative Reachability. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 504-518, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{brihaye_et_al:LIPIcs.CSL.2015.504, author = {Brihaye, Thomas and Bruy\`{e}re, V\'{e}ronique and Meunier, No\'{e}mie and Raskin, Jean-Francois}, title = {{Weak Subgame Perfect Equilibria and their Application to Quantitative Reachability}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {504--518}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.504}, URN = {urn:nbn:de:0030-drops-54345}, doi = {10.4230/LIPIcs.CSL.2015.504}, annote = {Keywords: multi-player games on graphs, quantitative objectives, Nash equilibrium, subgame perfect equilibrium, quantitative reachability} }
Felix Klein and Martin Zimmermann. What are Strategies in Delay Games? Borel Determinacy for Games with Lookahead. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 519-533, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{klein_et_al:LIPIcs.CSL.2015.519, author = {Klein, Felix and Zimmermann, Martin}, title = {{What are Strategies in Delay Games? Borel Determinacy for Games with Lookahead}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {519--533}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.519}, URN = {urn:nbn:de:0030-drops-54354}, doi = {10.4230/LIPIcs.CSL.2015.519}, annote = {Keywords: Determinacy, Infinite Games, Delay Games, Borel Hierarchy} }
Jacques Duparc, Kevin Fournier, and Szczepan Hummel. On Unambiguous Regular Tree Languages of Index (0,2). In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 534-548, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{duparc_et_al:LIPIcs.CSL.2015.534, author = {Duparc, Jacques and Fournier, Kevin and Hummel, Szczepan}, title = {{On Unambiguous Regular Tree Languages of Index (0,2)}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {534--548}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.534}, URN = {urn:nbn:de:0030-drops-54369}, doi = {10.4230/LIPIcs.CSL.2015.534}, annote = {Keywords: Tree Automata, Unambiguity, Wadge Hierarchy.} }
David Baelde, Amina Doumane, and Alexis Saurin. Least and Greatest Fixed Points in Ludics. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 549-566, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{baelde_et_al:LIPIcs.CSL.2015.549, author = {Baelde, David and Doumane, Amina and Saurin, Alexis}, title = {{Least and Greatest Fixed Points in Ludics}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {549--566}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.549}, URN = {urn:nbn:de:0030-drops-54374}, doi = {10.4230/LIPIcs.CSL.2015.549}, annote = {Keywords: proof theory, fixed points, linear logic, ludics, game semantics, completeness, circular proofs, infinitary proof systems} }
Flavien Breuvart and Michele Pagani. Modelling Coeffects in the Relational Semantics of Linear Logic. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 567-581, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{breuvart_et_al:LIPIcs.CSL.2015.567, author = {Breuvart, Flavien and Pagani, Michele}, title = {{Modelling Coeffects in the Relational Semantics of Linear Logic}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {567--581}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.567}, URN = {urn:nbn:de:0030-drops-54384}, doi = {10.4230/LIPIcs.CSL.2015.567}, annote = {Keywords: relational semantics, bounded linear logic, lambda calculus} }
Shahin Amini and Thomas Erhard. On Classical PCF, Linear Logic and the MIX Rule. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 582-596, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{amini_et_al:LIPIcs.CSL.2015.582, author = {Amini, Shahin and Erhard, Thomas}, title = {{On Classical PCF, Linear Logic and the MIX Rule}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {582--596}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.582}, URN = {urn:nbn:de:0030-drops-54402}, doi = {10.4230/LIPIcs.CSL.2015.582}, annote = {Keywords: lambda-calculus, linear logic, classical logic, denotational semantics} }
Emanuel Kierónski and Antti Kuusisto. Uniform One-Dimensional Fragments with One Equivalence Relation. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 597-615, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{kieronski_et_al:LIPIcs.CSL.2015.597, author = {Kier\'{o}nski, Emanuel and Kuusisto, Antti}, title = {{Uniform One-Dimensional Fragments with One Equivalence Relation}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {597--615}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.597}, URN = {urn:nbn:de:0030-drops-54418}, doi = {10.4230/LIPIcs.CSL.2015.597}, annote = {Keywords: two-variable logic, uniform one-dimensional fragments, complexity, expressivity, equivalence relations} }
Charles Paperman. Finite-Degree Predicates and Two-Variable First-Order Logic. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 616-630, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{paperman:LIPIcs.CSL.2015.616, author = {Paperman, Charles}, title = {{Finite-Degree Predicates and Two-Variable First-Order Logic}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {616--630}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.616}, URN = {urn:nbn:de:0030-drops-54420}, doi = {10.4230/LIPIcs.CSL.2015.616}, annote = {Keywords: First order logic, automata theory, semigroup, modular predicates} }
Witold Charatonik and Piotr Witkowski. Two-variable Logic with Counting and a Linear Order. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 631-647, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{charatonik_et_al:LIPIcs.CSL.2015.631, author = {Charatonik, Witold and Witkowski, Piotr}, title = {{Two-variable Logic with Counting and a Linear Order}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {631--647}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.631}, URN = {urn:nbn:de:0030-drops-54436}, doi = {10.4230/LIPIcs.CSL.2015.631}, annote = {Keywords: Two-variable logic, counting quantifiers, linear order, satisfiability, complexity} }
Fabio Mogavero and Giuseppe Perelli. Binding Forms in First-Order Logic. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 648-665, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{mogavero_et_al:LIPIcs.CSL.2015.648, author = {Mogavero, Fabio and Perelli, Giuseppe}, title = {{Binding Forms in First-Order Logic}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {648--665}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.648}, URN = {urn:nbn:de:0030-drops-54443}, doi = {10.4230/LIPIcs.CSL.2015.648}, annote = {Keywords: First-Order Logic, Decidable Fragments, Satisfiability, Model Checking} }
Feedback for Dagstuhl Publishing