@Proceedings{ronchidellarocca:LIPIcs.CSL.2013, title = {{LIPIcs, Volume 23, CSL'13, Complete Volume}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013}, URN = {urn:nbn:de:0030-drops-42618}, doi = {10.4230/LIPIcs.CSL.2013}, annote = {Keywords: Conference Proceedings, Theory of Computation, Distributed Systems, Software/ Programs Verifications, Formal Definitions and Theory Languages Constructs and Features, Knowledge Representations Formalisms and Methods} } @InProceedings{ronchidellarocca:LIPIcs.CSL.2013.i, author = {Ronchi Della Rocca, Simona}, title = {{Frontmatter, Table of Contents, Preface, Conference Organization}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {i--xiv}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.i}, URN = {urn:nbn:de:0030-drops-41821}, doi = {10.4230/LIPIcs.CSL.2013.i}, annote = {Keywords: Frontmatter, Table of Contents, Preface, Conference Organization} } @InProceedings{dawar_et_al:LIPIcs.CSL.2013.1, author = {Dawar, Anuj and Henzinger, Thomas A. and Niwi\'{n}ski, Damian}, title = {{The Ackermann Award 2013}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {1--4}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.1}, URN = {urn:nbn:de:0030-drops-41837}, doi = {10.4230/LIPIcs.CSL.2013.1}, annote = {Keywords: Ackermann award} } @InProceedings{dershowitz:LIPIcs.CSL.2013.5, author = {Dershowitz, Nachum}, title = {{Res Publica: The Universal Model of Computation}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {5--10}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.5}, URN = {urn:nbn:de:0030-drops-41844}, doi = {10.4230/LIPIcs.CSL.2013.5}, annote = {Keywords: Models of computation, cellular automata, abstract state machines, causal dynamics, interaction} } @InProceedings{girard:LIPIcs.CSL.2013.11, author = {Girard, Jean-Yves}, title = {{Three lightings of logic}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {11--23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.11}, URN = {urn:nbn:de:0030-drops-41852}, doi = {10.4230/LIPIcs.CSL.2013.11}, annote = {Keywords: Proof theory} } @InProceedings{oitavem:LIPIcs.CSL.2013.24, author = {Oitavem, Isabel}, title = {{From determinism, non-determinism and alternation to recursion schemes for P, NP and Pspace}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {24--27}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.24}, URN = {urn:nbn:de:0030-drops-41865}, doi = {10.4230/LIPIcs.CSL.2013.24}, annote = {Keywords: Computational complexity, Recursion schemes, P, NP, Pspace} } @InProceedings{tendera:LIPIcs.CSL.2013.28, author = {Tendera, Lidia}, title = {{Means and Limits of Decision}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {28--29}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.28}, URN = {urn:nbn:de:0030-drops-41870}, doi = {10.4230/LIPIcs.CSL.2013.28}, annote = {Keywords: classical decision problem, decidability, computational complexity, two-variable first-order logic, guarded logic} } @InProceedings{afshari_et_al:LIPIcs.CSL.2013.30, author = {Afshari, Bahareh and Leigh, Graham E.}, title = {{On closure ordinals for the modal mu-calculus}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {30--44}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.30}, URN = {urn:nbn:de:0030-drops-41889}, doi = {10.4230/LIPIcs.CSL.2013.30}, annote = {Keywords: Closure ordinals, Modal mu-calculus, Tableaux} } @InProceedings{aschieri_et_al:LIPIcs.CSL.2013.45, author = {Aschieri, Federico and Berardi, Stefano and Birolo, Giovanni}, title = {{Realizability and Strong Normalization for a Curry-Howard Interpretation of HA + EM1}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {45--60}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.45}, URN = {urn:nbn:de:0030-drops-41894}, doi = {10.4230/LIPIcs.CSL.2013.45}, annote = {Keywords: Interactive realizability, classical Arithmetic, witness extraction, delimited exceptions} } @InProceedings{berkholz_et_al:LIPIcs.CSL.2013.61, author = {Berkholz, Christoph and Krebs, Andreas and Verbitsky, Oleg}, title = {{Bounds for the quantifier depth in finite-variable logics: Alternation hierarchy}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {61--80}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.61}, URN = {urn:nbn:de:0030-drops-41907}, doi = {10.4230/LIPIcs.CSL.2013.61}, annote = {Keywords: Alternation hierarchy, finite-variable logic} } @InProceedings{bilkowski_et_al:LIPIcs.CSL.2013.81, author = {Bilkowski, Marcin and Skrzypczak, Micha{\l}}, title = {{Unambiguity and uniformization problems on infinite trees}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {81--100}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.81}, URN = {urn:nbn:de:0030-drops-41916}, doi = {10.4230/LIPIcs.CSL.2013.81}, annote = {Keywords: nondeterministic automata, infinite trees, MSO logic} } @InProceedings{boudes_et_al:LIPIcs.CSL.2013.101, author = {Boudes, Pierre and He, Fanny and Pagani, Michele}, title = {{A characterization of the Taylor expansion of lambda-terms}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {101--115}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.101}, URN = {urn:nbn:de:0030-drops-41925}, doi = {10.4230/LIPIcs.CSL.2013.101}, annote = {Keywords: Lambda-Calculus, B\"{o}hm trees, Differential Lambda-Calculus, Linear Logic} } @InProceedings{bradfield:LIPIcs.CSL.2013.116, author = {Bradfield, Julian}, title = {{Team building in dependence}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {116--128}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.116}, URN = {urn:nbn:de:0030-drops-41935}, doi = {10.4230/LIPIcs.CSL.2013.116}, annote = {Keywords: partially ordered quantification, independence-friendly logic, game semantics} } @InProceedings{broadbent_et_al:LIPIcs.CSL.2013.129, author = {Broadbent, Christopher and Kobayashi, Naoki}, title = {{Saturation-Based Model Checking of Higher-Order Recursion Schemes}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {129--148}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.129}, URN = {urn:nbn:de:0030-drops-41941}, doi = {10.4230/LIPIcs.CSL.2013.129}, annote = {Keywords: Model checking, higher-order recursion schemes, intersection types} } @InProceedings{bulatov_et_al:LIPIcs.CSL.2013.149, author = {Bulatov, Andrei and Dalmau, Victor and Thurley, Marc}, title = {{Descriptive complexity of approximate counting CSPs}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {149--164}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.149}, URN = {urn:nbn:de:0030-drops-41955}, doi = {10.4230/LIPIcs.CSL.2013.149}, annote = {Keywords: Constraint Satisfaction Problems, Approximate Counting, Descriptive Complexity} } @InProceedings{chatterjee_et_al:LIPIcs.CSL.2013.165, author = {Chatterjee, Krishnendu and Chmelik, Martin and Tracol, Mathieu}, title = {{What is Decidable about Partially Observable Markov Decision Processes with omega-Regular Objectives}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {165--180}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.165}, URN = {urn:nbn:de:0030-drops-41962}, doi = {10.4230/LIPIcs.CSL.2013.165}, annote = {Keywords: POMDPs, Omega-regular objectives, Parity objectives, Qualitative analysis} } @InProceedings{chatterjee_et_al:LIPIcs.CSL.2013.181, author = {Chatterjee, Krishnendu and Fijalkow, Nathana\"{e}l}, title = {{Infinite-state games with finitary conditions}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {181--196}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.181}, URN = {urn:nbn:de:0030-drops-41970}, doi = {10.4230/LIPIcs.CSL.2013.181}, annote = {Keywords: Two-player games, Infinite-state systems, Pushdown games, Bounds in omega-regularity, Synthesis} } @InProceedings{clouston_et_al:LIPIcs.CSL.2013.197, author = {Clouston, Ranald and Dawson, Jeremy and Gor\'{e}, Rajeev and Tiu, Alwen}, title = {{Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {197--214}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.197}, URN = {urn:nbn:de:0030-drops-41981}, doi = {10.4230/LIPIcs.CSL.2013.197}, annote = {Keywords: Linear logic, display calculus, nested sequent calculus, deep inference} } @InProceedings{colcombet_et_al:LIPIcs.CSL.2013.215, author = {Colcombet, Thomas and Kuperberg, Denis and L\"{o}ding, Christof and Vanden Boom, Michael}, title = {{Deciding the weak definability of B\"{u}chi definable tree languages}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {215--230}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.215}, URN = {urn:nbn:de:0030-drops-41998}, doi = {10.4230/LIPIcs.CSL.2013.215}, annote = {Keywords: Tree automata, weak definability, decidability, cost automata, boundedness} } @InProceedings{digianantonio_et_al:LIPIcs.CSL.2013.231, author = {Di Gianantonio, Pietro and Lenisa, Marina}, title = {{Innocent Game Semantics via Intersection Type Assignment Systems}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {231--247}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.231}, URN = {urn:nbn:de:0030-drops-42005}, doi = {10.4230/LIPIcs.CSL.2013.231}, annote = {Keywords: Game Semantics, Intersection Type Assignment System, Lambda Calculus} } @InProceedings{fortier_et_al:LIPIcs.CSL.2013.248, author = {Fortier, J\'{e}r\^{o}me and Santocanale, Luigi}, title = {{Cuts for circular proofs: semantics and cut-elimination}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {248--262}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.248}, URN = {urn:nbn:de:0030-drops-42019}, doi = {10.4230/LIPIcs.CSL.2013.248}, annote = {Keywords: categorical proof-theory, fixpoints, initial and final (co)algebras, inductive and coinductive types} } @InProceedings{galliani_et_al:LIPIcs.CSL.2013.263, author = {Galliani, Pietro and Hannula, Miika and Kontinen, Juha}, title = {{Hierarchies in independence logic}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {263--280}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.263}, URN = {urn:nbn:de:0030-drops-42021}, doi = {10.4230/LIPIcs.CSL.2013.263}, annote = {Keywords: Existential second-order logic, Independence logic, Inclusion logic, Expressiveness hierarchies} } @InProceedings{galliani_et_al:LIPIcs.CSL.2013.281, author = {Galliani, Pietro and Hella, Lauri}, title = {{Inclusion Logic and Fixed Point Logic}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {281--295}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.281}, URN = {urn:nbn:de:0030-drops-42031}, doi = {10.4230/LIPIcs.CSL.2013.281}, annote = {Keywords: Dependence Logic, Team Semantics, Fixpoint Logic, Inclusion} } @InProceedings{ghasemloo_et_al:LIPIcs.CSL.2013.296, author = {Ghasemloo, Kaveh and Cook, Stephen A.}, title = {{Theories for Subexponential-size Bounded-depth Frege Proofs}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {296--315}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.296}, URN = {urn:nbn:de:0030-drops-42044}, doi = {10.4230/LIPIcs.CSL.2013.296}, annote = {Keywords: Computational Complexity Theory, Proof Complexity, Bounded Arithmetic, NC1-Frege, AC0- Frege} } @InProceedings{gimenez_et_al:LIPIcs.CSL.2013.316, author = {Gimenez, St\'{e}phane and Moser, Georg}, title = {{The Structure of Interaction}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {316--331}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.316}, URN = {urn:nbn:de:0030-drops-42052}, doi = {10.4230/LIPIcs.CSL.2013.316}, annote = {Keywords: Interaction Nets, Linear Logic, Curry–Howard Correspondence, Deep Inference, Calculus of Structures, Strong Normalisation, Reducibility} } @InProceedings{goller:LIPIcs.CSL.2013.332, author = {G\"{o}ller, Stefan}, title = {{The Fixed-Parameter Tractability of Model Checking Concurrent Systems}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {332--347}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.332}, URN = {urn:nbn:de:0030-drops-42062}, doi = {10.4230/LIPIcs.CSL.2013.332}, annote = {Keywords: Model Checking, Concurrent Systems, Parameterized Complexity} } @InProceedings{hampson_et_al:LIPIcs.CSL.2013.348, author = {Hampson, Christopher and Kurucz, Agi}, title = {{One-variable first-order linear temporal logics with counting}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {348--362}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.348}, URN = {urn:nbn:de:0030-drops-42072}, doi = {10.4230/LIPIcs.CSL.2013.348}, annote = {Keywords: modal and temporal logic, counting, decision procedures} } @InProceedings{harwath_et_al:LIPIcs.CSL.2013.363, author = {Harwath, Frederik and Schweikardt, Nicole}, title = {{On the locality of arb-invariant first-order logic with modulo counting quantifiers}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {363--379}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.363}, URN = {urn:nbn:de:0030-drops-42086}, doi = {10.4230/LIPIcs.CSL.2013.363}, annote = {Keywords: finite model theory, Gaifman and Hanf locality, first-order logic with modulo counting quantifiers, order-invariant and arb-invariant formulas, lower} } @InProceedings{hunter:LIPIcs.CSL.2013.380, author = {Hunter, Paul}, title = {{When is Metric Temporal Logic Expressively Complete?}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {380--394}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.380}, URN = {urn:nbn:de:0030-drops-42092}, doi = {10.4230/LIPIcs.CSL.2013.380}, annote = {Keywords: Metric Temporal Logic, Expressive power, First-order logic} } @InProceedings{kikuchi:LIPIcs.CSL.2013.395, author = {Kikuchi, Kentaro}, title = {{Proving Strong Normalisation via Non-deterministic Translations into Klop's Extended lambda-Calculus}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {395--414}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.395}, URN = {urn:nbn:de:0030-drops-42108}, doi = {10.4230/LIPIcs.CSL.2013.395}, annote = {Keywords: Strong normalisation, Klop's extended lambda-calculus, Explicit substitution, Cut-elimination} } @InProceedings{kozen_et_al:LIPIcs.CSL.2013.415, author = {Kozen, Dexter and Mamouras, Konstantinos}, title = {{Kleene Algebra with Products and Iteration Theories}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {415--431}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.415}, URN = {urn:nbn:de:0030-drops-42111}, doi = {10.4230/LIPIcs.CSL.2013.415}, annote = {Keywords: Kleene algebra, typed Kleene algebra, iteration theories} } @InProceedings{krishnaswami_et_al:LIPIcs.CSL.2013.432, author = {Krishnaswami, Neelakantan R. and Dreyer, Derek}, title = {{Internalizing Relational Parametricity in the Extensional Calculus of Constructions}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {432--451}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.432}, URN = {urn:nbn:de:0030-drops-42125}, doi = {10.4230/LIPIcs.CSL.2013.432}, annote = {Keywords: Relational parametricity, dependent types, quasi-PERs} } @InProceedings{kuusisto:LIPIcs.CSL.2013.452, author = {Kuusisto, Antti}, title = {{Modal Logic and Distributed Message Passing Automata}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {452--468}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.452}, URN = {urn:nbn:de:0030-drops-42132}, doi = {10.4230/LIPIcs.CSL.2013.452}, annote = {Keywords: Modal logic, message passing automata, descriptive characterizations, distributed computing} } @InProceedings{leivant:LIPIcs.CSL.2013.469, author = {Leivant, Daniel}, title = {{Global semantic typing for inductive and coinductive computing}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {469--483}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.469}, URN = {urn:nbn:de:0030-drops-42142}, doi = {10.4230/LIPIcs.CSL.2013.469}, annote = {Keywords: Inductive and coinductive types, equational programs, intrinsic theories, global model theory} } @InProceedings{manuel_et_al:LIPIcs.CSL.2013.484, author = {Manuel, Amaldev and Zeume, Thomas}, title = {{Two-Variable Logic on 2-Dimensional Structures}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {484--499}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.484}, URN = {urn:nbn:de:0030-drops-42159}, doi = {10.4230/LIPIcs.CSL.2013.484}, annote = {Keywords: FO2, Data words, Satisfiability, Decidability, Automata} } @InProceedings{maruyama:LIPIcs.CSL.2013.500, author = {Maruyama, Yoshihiro}, title = {{Categorical Duality Theory: With Applications to Domains, Convexity, and the Distribution Monad}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {500--520}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.500}, URN = {urn:nbn:de:0030-drops-42168}, doi = {10.4230/LIPIcs.CSL.2013.500}, annote = {Keywords: duality, monad, categorical topology, domain theory, convex structure} } @InProceedings{materzok:LIPIcs.CSL.2013.521, author = {Materzok, Marek}, title = {{Axiomatizing Subtyped Delimited Continuations}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {521--539}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.521}, URN = {urn:nbn:de:0030-drops-42178}, doi = {10.4230/LIPIcs.CSL.2013.521}, annote = {Keywords: Delimited Continuations, Continuation Passing Style, Axiomatization} } @InProceedings{mellies:LIPIcs.CSL.2013.540, author = {Melli\`{e}s, Paul-Andr\'{e}}, title = {{On dialogue games and coherent strategies}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {540--562}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.540}, URN = {urn:nbn:de:0030-drops-42181}, doi = {10.4230/LIPIcs.CSL.2013.540}, annote = {Keywords: Game semantics, Stable order, Extensional order, Bistructures, Tensorial logic, Innocent strategies} } @InProceedings{michaliszyn_et_al:LIPIcs.CSL.2013.563, author = {Michaliszyn, Jakub and Otop, Jan}, title = {{Elementary Modal Logics over Transitive Structures}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {563--577}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.563}, URN = {urn:nbn:de:0030-drops-42195}, doi = {10.4230/LIPIcs.CSL.2013.563}, annote = {Keywords: Modal logic, Transitive frames, Elementary modal logics, Decidability} } @InProceedings{nishimura:LIPIcs.CSL.2013.578, author = {Nishimura, Susumu}, title = {{A Fully Abstract Game Semantics for Parallelism with Non-Blocking Synchronization on Shared Variables}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {578--596}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.578}, URN = {urn:nbn:de:0030-drops-42201}, doi = {10.4230/LIPIcs.CSL.2013.578}, annote = {Keywords: shared variable parallelism, non-blocking synchronization, full abstraction, game semantics} } @InProceedings{rieg:LIPIcs.CSL.2013.597, author = {Rieg, Lionel}, title = {{Extracting Herbrand trees in classical realizability using forcing}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {597--614}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.597}, URN = {urn:nbn:de:0030-drops-42212}, doi = {10.4230/LIPIcs.CSL.2013.597}, annote = {Keywords: classical realizability, forcing, Curry-Howard correspondence, Herbrand trees} } @InProceedings{schmidt_et_al:LIPIcs.CSL.2013.615, author = {Schmidt, Johannes and Wrona, Micha{\l}}, title = {{The Complexity of Abduction for Equality Constraint Languages}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {615--633}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.615}, URN = {urn:nbn:de:0030-drops-42229}, doi = {10.4230/LIPIcs.CSL.2013.615}, annote = {Keywords: Abduction, infinite structures, equality constraint languages, computational complexity, algebraic approach} } @InProceedings{statman:LIPIcs.CSL.2013.634, author = {Statman, Rick}, title = {{A New Type Assignment for Strongly Normalizable Terms}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {634--652}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.634}, URN = {urn:nbn:de:0030-drops-42233}, doi = {10.4230/LIPIcs.CSL.2013.634}, annote = {Keywords: lambda calculus} } @InProceedings{wang_et_al:LIPIcs.CSL.2013.653, author = {Wang, Qian and Barras, Bruno}, title = {{Semantics of Intensional Type Theory extended with Decidable Equational Theories}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {653--667}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.653}, URN = {urn:nbn:de:0030-drops-42241}, doi = {10.4230/LIPIcs.CSL.2013.653}, annote = {Keywords: Calculus of Constructions, Extensional Type Theory, Intensional Type Theory, Model, Meta-theory, Consistency, Strong Normalization, Presburger Arithme} }
The metadata provided by Dagstuhl Publishing on its webpages, as well as their export formats (such as XML or BibTeX) available at our website, is released under the CC0 1.0 Public Domain Dedication license. That is, you are free to copy, distribute, use, modify, transform, build upon, and produce derived works from our data, even for commercial purposes, all without asking permission. Of course, we are always happy if you provide a link to us as the source of the data.
Read the full CC0 1.0 legal code for the exact terms that apply: https://creativecommons.org/publicdomain/zero/1.0/legalcode
Feedback for Dagstuhl Publishing