45 Search Results for "Jung, Achim"

Volume

LIPIcs, Volume 119

27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

CSL 2018, September 4-7, 2018, Birmingham, GB

Editors: Dan R. Ghica and Achim Jung

Document
Complete Volume
DOI: 10.4230/LIPIcs.CSL.2018
LIPIcs, Volume 119, CSL'18, Complete Volume

Authors: Dan Ghica and Achim Jung

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
LIPIcs, Volume 119, CSL'18, Complete Volume
Cite as

27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Proceedings{ghica_et_al:LIPIcs.CSL.2018,
  title =	{{LIPIcs, Volume 119, CSL'18, Complete Volume}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018},
  URN =		{urn:nbn:de:0030-drops-97444},
  doi =		{10.4230/LIPIcs.CSL.2018},
  annote =	{Keywords: Theory of computation, Software and its engineering, Formal language definitions, Formal software verification}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.CSL.2018.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Dan R. Ghica and Achim Jung

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{ghica_et_al:LIPIcs.CSL.2018.0,
  author =	{Ghica, Dan R. and Jung, Achim},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{0:i--0:xiv},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.0},
  URN =		{urn:nbn:de:0030-drops-96679},
  doi =		{10.4230/LIPIcs.CSL.2018.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.1
The Ackermann Award 2018

Authors: Dexter Kozen and Thomas Schwentick

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
The Ackermann Award is the EACSL Outstanding Dissertation Award for Logic in Computer Science. It is presented during the annual conference of the EACSL (CSL'xx). This contribution reports on the 2018 edition of the award.
Cite as

Dexter Kozen and Thomas Schwentick. The Ackermann Award 2018. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 1:1-1:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{kozen_et_al:LIPIcs.CSL.2018.1,
  author =	{Kozen, Dexter and Schwentick, Thomas},
  title =	{{The Ackermann Award 2018}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{1:1--1:5},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.1},
  URN =		{urn:nbn:de:0030-drops-96686},
  doi =		{10.4230/LIPIcs.CSL.2018.1},
  annote =	{Keywords: Ackermann Award}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.2
Relating Structure and Power: Comonadic Semantics for Computational Resources

Authors: Samson Abramsky and Nihil Shah

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
Combinatorial games are widely used in finite model theory, constraint satisfaction, modal logic and concurrency theory to characterize logical equivalences between structures. In particular, Ehrenfeucht-Fraïssé games, pebble games, and bisimulation games play a central role. We show how each of these types of games can be described in terms of an indexed family of comonads on the category of relational structures and homomorphisms. The index k is a resource parameter which bounds the degree of access to the underlying structure. The coKleisli categories for these comonads can be used to give syntax-free characterizations of a wide range of important logical equivalences. Moreover, the coalgebras for these indexed comonads can be used to characterize key combinatorial parameters: tree-depth for the Ehrenfeucht-Fraïssé comonad, tree-width for the pebbling comonad, and synchronization-tree depth for the modal unfolding comonad. These results pave the way for systematic connections between two major branches of the field of logic in computer science which hitherto have been almost disjoint: categorical semantics, and finite and algorithmic model theory.
Cite as

Samson Abramsky and Nihil Shah. Relating Structure and Power: Comonadic Semantics for Computational Resources. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 2:1-2:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{abramsky_et_al:LIPIcs.CSL.2018.2,
  author =	{Abramsky, Samson and Shah, Nihil},
  title =	{{Relating Structure and Power: Comonadic Semantics for Computational Resources}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{2:1--2:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.2},
  URN =		{urn:nbn:de:0030-drops-96698},
  doi =		{10.4230/LIPIcs.CSL.2018.2},
  annote =	{Keywords: Finite model theory, combinatorial games, Ehrenfeucht-Fra\"{i}ss\'{e} games, pebble games, bisimulation, comonads, coKleisli category, coalgebras of a comonad}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.3
Climbing up the Elementary Complexity Classes with Theories of Automatic Structures

Authors: Faried Abu Zaid, Dietrich Kuske, and Peter Lindner

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
Automatic structures are structures that admit a finite presentation via automata. Their most prominent feature is that their theories are decidable. In the literature, one finds automatic structures with non-elementary theory (e.g., the complete binary tree with equal-level predicate) and automatic structures whose theories are at most 3-fold exponential (e.g., Presburger arithmetic or infinite automatic graphs of bounded degree). This observation led Durand-Gasselin to the question whether there are automatic structures of arbitrary high elementary complexity. We give a positive answer to this question. Namely, we show that for every h >=0 the forest of (infinitely many copies of) all finite trees of height at most h+2 is automatic and it's theory is complete for STA(*, exp_h(n, poly(n)), poly(n)), an alternating complexity class between h-fold exponential time and space. This exact determination of the complexity of the theory of these forests might be of independent interest.
Cite as

Faried Abu Zaid, Dietrich Kuske, and Peter Lindner. Climbing up the Elementary Complexity Classes with Theories of Automatic Structures. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 3:1-3:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{abuzaid_et_al:LIPIcs.CSL.2018.3,
  author =	{Abu Zaid, Faried and Kuske, Dietrich and Lindner, Peter},
  title =	{{Climbing up the Elementary Complexity Classes with Theories of Automatic Structures}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{3:1--3:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.3},
  URN =		{urn:nbn:de:0030-drops-96701},
  doi =		{10.4230/LIPIcs.CSL.2018.3},
  annote =	{Keywords: Automatic Structures, Complexity Theory, Model Theory}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.4
High-Level Signatures and Initial Semantics

Authors: Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, and Marco Maggesi

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
We present a device for specifying and reasoning about syntax for datatypes, programming languages, and logic calculi. More precisely, we consider a general notion of "signature" for specifying syntactic constructions. Our signatures subsume classical algebraic signatures (i.e., signatures for languages with variable binding, such as the pure lambda calculus) and extend to much more general examples. In the spirit of Initial Semantics, we define the "syntax generated by a signature" to be the initial object - if it exists - in a suitable category of models. Our notions of signature and syntax are suited for compositionality and provide, beyond the desired algebra of terms, a well-behaved substitution and the associated inductive/recursive principles. Our signatures are "general" in the sense that the existence of an associated syntax is not automatically guaranteed. In this work, we identify a large and simple class of signatures which do generate a syntax. This paper builds upon ideas from a previous attempt by Hirschowitz-Maggesi, which, in turn, was directly inspired by some earlier work of Ghani-Uustalu-Hamana and Matthes-Uustalu. The main results presented in the paper are computer-checked within the UniMath system.
Cite as

Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, and Marco Maggesi. High-Level Signatures and Initial Semantics. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 4:1-4:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{ahrens_et_al:LIPIcs.CSL.2018.4,
  author =	{Ahrens, Benedikt and Hirschowitz, Andr\'{e} and Lafont, Ambroise and Maggesi, Marco},
  title =	{{High-Level Signatures and Initial Semantics}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{4:1--4:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.4},
  URN =		{urn:nbn:de:0030-drops-96713},
  doi =		{10.4230/LIPIcs.CSL.2018.4},
  annote =	{Keywords: initial semantics, signatures, syntax, monadic substitution, computer-checked proofs}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.5
The True Concurrency of Herbrand's Theorem

Authors: Aurore Alcolei, Pierre Clairambault, Martin Hyland, and Glynn Winskel

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
Herbrand's theorem, widely regarded as a cornerstone of proof theory, exposes some of the constructive content of classical logic. In its simplest form, it reduces the validity of a first-order purely existential formula to that of a finite disjunction. In the general case, it reduces first-order validity to propositional validity, by understanding the structure of the assignment of first-order terms to existential quantifiers, and the causal dependency between quantifiers. In this paper, we show that Herbrand's theorem in its general form can be elegantly stated and proved as a theorem in the framework of concurrent games, a denotational semantics designed to faithfully represent causality and independence in concurrent systems, thereby exposing the concurrency underlying the computational content of classical proofs. The causal structure of concurrent strategies, paired with annotations by first-order terms, is used to specify the dependency between quantifiers implicit in proofs. Furthermore concurrent strategies can be composed, yielding a compositional proof of Herbrand's theorem, simply by interpreting classical sequent proofs in a well-chosen denotational model.
Cite as

Aurore Alcolei, Pierre Clairambault, Martin Hyland, and Glynn Winskel. The True Concurrency of Herbrand's Theorem. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 5:1-5:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{alcolei_et_al:LIPIcs.CSL.2018.5,
  author =	{Alcolei, Aurore and Clairambault, Pierre and Hyland, Martin and Winskel, Glynn},
  title =	{{The True Concurrency of Herbrand's Theorem}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{5:1--5:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.5},
  URN =		{urn:nbn:de:0030-drops-96723},
  doi =		{10.4230/LIPIcs.CSL.2018.5},
  annote =	{Keywords: Herbrand's theorem, Game semantics, True concurrency}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.6
Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities

Authors: Carlo Angiuli, Kuen-Bang Hou (Favonia), and Robert Harper

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
We present a dependent type theory organized around a Cartesian notion of cubes (with faces, degeneracies, and diagonals), supporting both fibrant and non-fibrant types. The fibrant fragment validates Voevodsky's univalence axiom and includes a circle type, while the non-fibrant fragment includes exact (strict) equality types satisfying equality reflection. Our type theory is defined by a semantics in cubical partial equivalence relations, and is the first two-level type theory to satisfy the canonicity property: all closed terms of boolean type evaluate to either true or false.
Cite as

Carlo Angiuli, Kuen-Bang Hou (Favonia), and Robert Harper. Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{angiuli_et_al:LIPIcs.CSL.2018.6,
  author =	{Angiuli, Carlo and Hou (Favonia), Kuen-Bang and Harper, Robert},
  title =	{{Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{6:1--6:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.6},
  URN =		{urn:nbn:de:0030-drops-96734},
  doi =		{10.4230/LIPIcs.CSL.2018.6},
  annote =	{Keywords: Homotopy Type Theory, Two-Level Type Theory, Computational Type Theory, Cubical Sets}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.7
Definable Inapproximability: New Challenges for Duplicator

Authors: Albert Atserias and Anuj Dawar

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
We consider the hardness of approximation of optimization problems from the point of view of definability. For many NP-hard optimization problems it is known that, unless P = NP, no polynomial-time algorithm can give an approximate solution guaranteed to be within a fixed constant factor of the optimum. We show, in several such instances and without any complexity theoretic assumption, that no algorithm that is expressible in fixed-point logic with counting (FPC) can compute an approximate solution. Since important algorithmic techniques for approximation algorithms (such as linear or semidefinite programming) are expressible in FPC, this yields lower bounds on what can be achieved by such methods. The results are established by showing lower bounds on the number of variables required in first-order logic with counting to separate instances with a high optimum from those with a low optimum for fixed-size instances.
Cite as

Albert Atserias and Anuj Dawar. Definable Inapproximability: New Challenges for Duplicator. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 7:1-7:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{atserias_et_al:LIPIcs.CSL.2018.7,
  author =	{Atserias, Albert and Dawar, Anuj},
  title =	{{Definable Inapproximability: New Challenges for Duplicator}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{7:1--7:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.7},
  URN =		{urn:nbn:de:0030-drops-96742},
  doi =		{10.4230/LIPIcs.CSL.2018.7},
  annote =	{Keywords: Descriptive Compleixty, Hardness of Approximation, MAX SAT, Vertex Cover, Fixed-point logic with counting}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.8
Safety, Absoluteness, and Computability

Authors: Arnon Avron, Shahar Lev, and Nissan Levi

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
The semantic notion of dependent safety is a common generalization of the notion of absoluteness used in set theory and the notion of domain independence used in database theory for characterizing safe queries. This notion has been used in previous works to provide a unified theory of constructions and operations as they are used in different branches of mathematics and computer science, including set theory, computability theory, and database theory. In this paper we provide a complete syntactic characterization of general first-order dependent safety. We also show that this syntactic safety relation can be used for characterizing the set of strictly decidable relations on the natural numbers, as well as for characterizing rudimentary set theory and absoluteness of formulas within it.
Cite as

Arnon Avron, Shahar Lev, and Nissan Levi. Safety, Absoluteness, and Computability. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{avron_et_al:LIPIcs.CSL.2018.8,
  author =	{Avron, Arnon and Lev, Shahar and Levi, Nissan},
  title =	{{Safety, Absoluteness, and Computability}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{8:1--8:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.8},
  URN =		{urn:nbn:de:0030-drops-96754},
  doi =		{10.4230/LIPIcs.CSL.2018.8},
  annote =	{Keywords: Dependent Safety, Computability, Absoluteness, Decidability, Domain Independence}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.9
Combining Linear Logic and Size Types for Implicit Complexity

Authors: Patrick Baillot and Alexis Ghyselen

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
Several type systems have been proposed to statically control the time complexity of lambda-calculus programs and characterize complexity classes such as FPTIME or FEXPTIME. A first line of research stems from linear logic and restricted versions of its !-modality controlling duplication. A second approach relies on the idea of tracking the size increase between input and output, and together with a restricted recursion scheme, to deduce time complexity bounds. However both approaches suffer from limitations : either a limited intensional expressivity, or linearity restrictions. In the present work we incorporate both approaches into a common type system, in order to overcome their respective constraints. Our system is based on elementary linear logic combined with linear size types, called sEAL, and leads to characterizations of the complexity classes FPTIME and 2k-FEXPTIME, for k >= 0.
Cite as

Patrick Baillot and Alexis Ghyselen. Combining Linear Logic and Size Types for Implicit Complexity. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 9:1-9:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{baillot_et_al:LIPIcs.CSL.2018.9,
  author =	{Baillot, Patrick and Ghyselen, Alexis},
  title =	{{Combining Linear Logic and Size Types for Implicit Complexity}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{9:1--9:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.9},
  URN =		{urn:nbn:de:0030-drops-96763},
  doi =		{10.4230/LIPIcs.CSL.2018.9},
  annote =	{Keywords: Implicit computational complexity, lambda-calculus, linear logic, type systems, polynomial time complexity, size types}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.10
Beyond Admissibility: Dominance Between Chains of Strategies

Authors: Nicolas Basset, Ismaël Jecker, Arno Pauly, Jean-François Raskin, and Marie Van den Bogaard

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
Admissible strategies, i.e. those that are not dominated by any other strategy, are a typical rationality notion in game theory. In many classes of games this is justified by results showing that any strategy is admissible or dominated by an admissible strategy. However, in games played on finite graphs with quantitative objectives (as used for reactive synthesis), this is not the case. We consider increasing chains of strategies instead to recover a satisfactory rationality notion based on dominance in such games. We start with some order-theoretic considerations establishing sufficient criteria for this to work. We then turn our attention to generalised safety/reachability games as a particular application. We propose the notion of maximal uniform chain as the desired dominance-based rationality concept in these games. Decidability of some fundamental questions about uniform chains is established.
Cite as

Nicolas Basset, Ismaël Jecker, Arno Pauly, Jean-François Raskin, and Marie Van den Bogaard. Beyond Admissibility: Dominance Between Chains of Strategies. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 10:1-10:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{basset_et_al:LIPIcs.CSL.2018.10,
  author =	{Basset, Nicolas and Jecker, Isma\"{e}l and Pauly, Arno and Raskin, Jean-Fran\c{c}ois and Van den Bogaard, Marie},
  title =	{{Beyond Admissibility: Dominance Between Chains of Strategies}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{10:1--10:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.10},
  URN =		{urn:nbn:de:0030-drops-96774},
  doi =		{10.4230/LIPIcs.CSL.2018.10},
  annote =	{Keywords: dominated strategies, admissible strategies, games played on finite graphs, reactive synthesis, reachability games, safety games, cofinal, order theory}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.11
Rule Algebras for Adhesive Categories

Authors: Nicolas Behr and Pawel Sobocinski

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
We show that every adhesive category gives rise to an associative algebra of rewriting rules induced by the notion of double-pushout (DPO) rewriting and the associated notion of concurrent production. In contrast to the original formulation of rule algebras in terms of relations between (a concrete notion of) graphs, here we work in an abstract categorical setting. Doing this, we extend the classical concurrency theorem of DPO rewriting and show that the composition of DPO rules along abstract dependency relations is, in a natural sense, an associative operation. If in addition the adhesive category possesses a strict initial object, the resulting rule algebra is also unital. We demonstrate that in this setting the canonical representation of the rule algebras is obtainable, which opens the possibility of applying the concept to define and compute the evolution of statistical moments of observables in stochastic DPO rewriting systems.
Cite as

Nicolas Behr and Pawel Sobocinski. Rule Algebras for Adhesive Categories. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 11:1-11:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{behr_et_al:LIPIcs.CSL.2018.11,
  author =	{Behr, Nicolas and Sobocinski, Pawel},
  title =	{{Rule Algebras for Adhesive Categories}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{11:1--11:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.11},
  URN =		{urn:nbn:de:0030-drops-96781},
  doi =		{10.4230/LIPIcs.CSL.2018.11},
  annote =	{Keywords: Adhesive categories, rule algebras, Double Pushout (DPO) rewriting}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.12
Submodular Functions and Valued Constraint Satisfaction Problems over Infinite Domains

Authors: Manuel Bodirsky, Marcello Mamino, and Caterina Viola

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
Valued constraint satisfaction problems (VCSPs) are a large class of combinatorial optimisation problems. It is desirable to classify the computational complexity of VCSPs depending on a fixed set of allowed cost functions in the input. Recently, the computational complexity of all VCSPs for finite sets of cost functions over finite domains has been classified in this sense. Many natural optimisation problems, however, cannot be formulated as VCSPs over a finite domain. We initiate the systematic investigation of infinite-domain VCSPs by studying the complexity of VCSPs for piecewise linear homogeneous cost functions. We remark that in this paper the infinite domain will always be the set of rational numbers. We show that such VCSPs can be solved in polynomial time when the cost functions are additionally submodular, and that this is indeed a maximally tractable class: adding any cost function that is not submodular leads to an NP-hard VCSP.
Cite as

Manuel Bodirsky, Marcello Mamino, and Caterina Viola. Submodular Functions and Valued Constraint Satisfaction Problems over Infinite Domains. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 12:1-12:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{bodirsky_et_al:LIPIcs.CSL.2018.12,
  author =	{Bodirsky, Manuel and Mamino, Marcello and Viola, Caterina},
  title =	{{Submodular Functions and Valued Constraint Satisfaction Problems over Infinite Domains}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{12:1--12:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.12},
  URN =		{urn:nbn:de:0030-drops-96792},
  doi =		{10.4230/LIPIcs.CSL.2018.12},
  annote =	{Keywords: Valued constraint satisfaction problems, Piecewise linear functions, Submodular functions, Semilinear, Constraint satisfaction, Optimisation, Model Theory}
}
  • Refine by Author
  • 7 Jung, Achim
  • 2 Clairambault, Pierre
  • 2 Das, Anupam
  • 2 Dawar, Anuj
  • 2 Ghica, Dan R.
  • Show More...

  • Refine by Classification
  • 6 Theory of computation → Proof theory
  • 5 Theory of computation → Complexity theory and logic
  • 5 Theory of computation → Finite Model Theory
  • 4 Theory of computation → Categorical semantics
  • 4 Theory of computation → Denotational semantics
  • Show More...

  • Refine by Keyword
  • 3 linear logic
  • 2 Expressive power
  • 2 Infinite Games
  • 2 Model Theory
  • 2 domain theory
  • Show More...

  • Refine by Type
  • 44 document
  • 1 volume

  • Refine by Publication Year
  • 40 2018
  • 2 2017
  • 1 1999
  • 1 2005
  • 1 2016

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact