@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}
}