Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. i-xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Anuj Dawar, Thomas A. Henzinger, and Damian Niwiński. The Ackermann Award 2013. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 1-4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Nachum Dershowitz. Res Publica: The Universal Model of Computation (Invited Talk). In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 5-10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Jean-Yves Girard. Three lightings of logic (Invited Talk). In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 11-23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Isabel Oitavem. From determinism, non-determinism and alternation to recursion schemes for P, NP and Pspace (Invited Talk). In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 24-27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Lidia Tendera. Means and Limits of Decision (Invited Talk). In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 28-29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Bahareh Afshari and Graham E. Leigh. On closure ordinals for the modal mu-calculus. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 30-44, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Federico Aschieri, Stefano Berardi, and Giovanni Birolo. Realizability and Strong Normalization for a Curry-Howard Interpretation of HA + EM1. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 45-60, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Christoph Berkholz, Andreas Krebs, and Oleg Verbitsky. Bounds for the quantifier depth in finite-variable logics: Alternation hierarchy. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 61-80, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Marcin Bilkowski and Michał Skrzypczak. Unambiguity and uniformization problems on infinite trees. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 81-100, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Pierre Boudes, Fanny He, and Michele Pagani. A characterization of the Taylor expansion of lambda-terms. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 101-115, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Julian Bradfield. Team building in dependence. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 116-128, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Christopher Broadbent and Naoki Kobayashi. Saturation-Based Model Checking of Higher-Order Recursion Schemes. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 129-148, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Andrei Bulatov, Victor Dalmau, and Marc Thurley. Descriptive complexity of approximate counting CSPs. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 149-164, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Krishnendu Chatterjee, Martin Chmelik, and Mathieu Tracol. What is Decidable about Partially Observable Markov Decision Processes with omega-Regular Objectives. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 165-180, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Krishnendu Chatterjee and Nathanaël Fijalkow. Infinite-state games with finitary conditions. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 181-196, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Ranald Clouston, Jeremy Dawson, Rajeev Goré, and Alwen Tiu. Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 197-214, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Thomas Colcombet, Denis Kuperberg, Christof Löding, and Michael Vanden Boom. Deciding the weak definability of Büchi definable tree languages. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 215-230, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Pietro Di Gianantonio and Marina Lenisa. Innocent Game Semantics via Intersection Type Assignment Systems. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 231-247, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Jérôme Fortier and Luigi Santocanale. Cuts for circular proofs: semantics and cut-elimination. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 248-262, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Pietro Galliani, Miika Hannula, and Juha Kontinen. Hierarchies in independence logic. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 263-280, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Pietro Galliani and Lauri Hella. Inclusion Logic and Fixed Point Logic. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 281-295, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Kaveh Ghasemloo and Stephen A. Cook. Theories for Subexponential-size Bounded-depth Frege Proofs. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 296-315, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Stéphane Gimenez and Georg Moser. The Structure of Interaction. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 316-331, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Stefan Göller. The Fixed-Parameter Tractability of Model Checking Concurrent Systems. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 332-347, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Christopher Hampson and Agi Kurucz. One-variable first-order linear temporal logics with counting. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 348-362, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Frederik Harwath and Nicole Schweikardt. On the locality of arb-invariant first-order logic with modulo counting quantifiers. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 363-379, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Paul Hunter. When is Metric Temporal Logic Expressively Complete?. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 380-394, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Kentaro Kikuchi. Proving Strong Normalisation via Non-deterministic Translations into Klop's Extended lambda-Calculus. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 395-414, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Dexter Kozen and Konstantinos Mamouras. Kleene Algebra with Products and Iteration Theories. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 415-431, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Neelakantan R. Krishnaswami and Derek Dreyer. Internalizing Relational Parametricity in the Extensional Calculus of Constructions. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 432-451, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Antti Kuusisto. Modal Logic and Distributed Message Passing Automata. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 452-468, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Daniel Leivant. Global semantic typing for inductive and coinductive computing. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 469-483, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Amaldev Manuel and Thomas Zeume. Two-Variable Logic on 2-Dimensional Structures. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 484-499, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Yoshihiro Maruyama. Categorical Duality Theory: With Applications to Domains, Convexity, and the Distribution Monad. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 500-520, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Marek Materzok. Axiomatizing Subtyped Delimited Continuations. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 521-539, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Paul-André Melliès. On dialogue games and coherent strategies. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 540-562, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Jakub Michaliszyn and Jan Otop. Elementary Modal Logics over Transitive Structures. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 563-577, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Susumu Nishimura. A Fully Abstract Game Semantics for Parallelism with Non-Blocking Synchronization on Shared Variables. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 578-596, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Lionel Rieg. Extracting Herbrand trees in classical realizability using forcing. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 597-614, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Johannes Schmidt and Michał Wrona. The Complexity of Abduction for Equality Constraint Languages. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 615-633, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Rick Statman. A New Type Assignment for Strongly Normalizable Terms. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 634-652, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Qian Wang and Bruno Barras. Semantics of Intensional Type Theory extended with Decidable Equational Theories. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 653-667, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Feedback for Dagstuhl Publishing