54 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
DOI: 10.4230/LIPIcs.CSL.2026.12
String Diagrams for Closed Symmetric Monoidal Categories

Authors: Callum Reader and Alessandro Di Giorgio

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
We introduce a graphical language for closed symmetric monoidal categories based on an extension of string diagrams with special bracket wires representing internal homs. These bracket wires make the structure of the internal hom functor explicit, allowing standard morphism wires to interact with them through a well-defined set of graphical rules. We establish the soundness and completeness of the diagrammatic calculus, and illustrate its expressiveness through examples drawn from category theory, logic and programming language semantics.
Cite as

Callum Reader and Alessandro Di Giorgio. String Diagrams for Closed Symmetric Monoidal Categories. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 12:1-12:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{reader_et_al:LIPIcs.CSL.2026.12,
  author =	{Reader, Callum and Di Giorgio, Alessandro},
  title =	{{String Diagrams for Closed Symmetric Monoidal Categories}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{12:1--12:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.12},
  URN =		{urn:nbn:de:0030-drops-254369},
  doi =		{10.4230/LIPIcs.CSL.2026.12},
  annote =	{Keywords: diagrammatic languages, logic, lambda calculi}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.33
Scott’s Representation Theorem and the Univalent Karoubi Envelope

Authors: Arnoud van der Leer, Kobe Wullaert, and Benedikt Ahrens

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Lambek and Scott constructed a correspondence between simply-typed lambda calculi and Cartesian closed categories. Scott’s Representation Theorem is a cousin to this result for untyped lambda calculi. It states that every untyped lambda calculus arises from a reflexive object in some category. We present a formalization of Scott’s Representation Theorem in univalent foundations, in the (Rocq-)UniMath library. Specifically, we implement two proofs of that theorem, one by Scott and one by Hyland. We also explain the role of the Karoubi envelope - a categorical construction - in the proofs and the impact the chosen foundation has on this construction. Finally, we report on some automation we have implemented for the reduction of λ-terms.
Cite as

Arnoud van der Leer, Kobe Wullaert, and Benedikt Ahrens. Scott’s Representation Theorem and the Univalent Karoubi Envelope. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 33:1-33:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{vanderleer_et_al:LIPIcs.ITP.2025.33,
  author =	{van der Leer, Arnoud and Wullaert, Kobe and Ahrens, Benedikt},
  title =	{{Scott’s Representation Theorem and the Univalent Karoubi Envelope}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{33:1--33:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.33},
  URN =		{urn:nbn:de:0030-drops-246318},
  doi =		{10.4230/LIPIcs.ITP.2025.33},
  annote =	{Keywords: Lambda calculi, algebraic theories, categorical semantics, Karoubi envelope, formalization, Rocq-UniMath, univalent foundations}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.39
Right-Linear Lattices: An Algebraic Theory of ω-Regular Languages, with Fixed Points

Authors: Anupam Das and Abhishek De

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
Alternating parity automata (APAs) provide a robust formalism for modelling infinite behaviours and play a central role in formal verification. Despite their widespread use, the algebraic theory underlying APAs has remained largely unexplored. In recent work [Anupam Das and Abhishek De, 2024], a notation for non-deterministic finite automata (NFAs) was introduced, along with a sound and complete axiomatisation of their equational theory via right-linear algebras. In this paper, we extend that line of work to the setting of infinite words. In particular, we present a dualised syntax, yielding a notation for APAs based on right-linear lattice expressions, and provide a natural axiomatisation of their equational theory with respect to the standard language model of ω-regular languages. The design of this axiomatisation is guided by the theory of fixed point logics; in fact, the completeness factors cleanly through the completeness of the linear-time μ-calculus.
Cite as

Anupam Das and Abhishek De. Right-Linear Lattices: An Algebraic Theory of ω-Regular Languages, with Fixed Points. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 39:1-39:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{das_et_al:LIPIcs.MFCS.2025.39,
  author =	{Das, Anupam and De, Abhishek},
  title =	{{Right-Linear Lattices: An Algebraic Theory of \omega-Regular Languages, with Fixed Points}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{39:1--39:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.39},
  URN =		{urn:nbn:de:0030-drops-241461},
  doi =		{10.4230/LIPIcs.MFCS.2025.39},
  annote =	{Keywords: omega-languages, regular languages, fixed points, Kleene algebras, right-linear grammars}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.23
∞-Categorical Models of Linear Logic

Authors: Eliès Harington and Samuel Mimram

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
The notion of categorical model of linear logic is now well studied and established around the notion of linear-non-linear adjunction, which encompasses the earlier notions of Seely categories, Lafont categories and linear categories. These categorical structures have counterparts in the realm of ∞-categories, which can thus be thought of as weak forms of models of linear logic. The goal of this article is to formally introduce them and study their relationships. We show that ∞-linear-non-linear adjunctions still play the role of a unifying notion of model in this setting. Moreover, we provide a sufficient condition for a symmetric monoidal ∞-category to be Lafont. Finally, we illustrate our constructions by providing models: we construct linear-non-linear adjunctions that generalize well-known models in relations (and variants based on profunctors or spans), domains and vector spaces. In particular, we introduce a model based on spectra, a homotopical variant of abelian groups.
Cite as

Eliès Harington and Samuel Mimram. ∞-Categorical Models of Linear Logic. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 23:1-23:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{harington_et_al:LIPIcs.FSCD.2025.23,
  author =	{Harington, Eli\`{e}s and Mimram, Samuel},
  title =	{{∞-Categorical Models of Linear Logic}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{23:1--23:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.23},
  URN =		{urn:nbn:de:0030-drops-236381},
  doi =		{10.4230/LIPIcs.FSCD.2025.23},
  annote =	{Keywords: linear logic, linear-non-linear adjunction, ∞-category, spectrum}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2024.4
Separating Terms by Means of Multi Types, Coinductively

Authors: Adrienne Lancelot

Published in: LIPIcs, Volume 336, 30th International Conference on Types for Proofs and Programs (TYPES 2024)

Abstract
Intersection type systems, as adequate models of the λ-calculus, induce an equational theory on terms, that we refer to as type equivalence. We give a new proof technique to coinductively characterize type equivalence. To do so, we explore a simple setting, namely weak head type equivalence, which is the equational theory induced by a weak head non-idempotent intersection type system. We prove a folklore result: weak head type equivalence coincides with Sangiorgi’s normal form bisimilarity. What is new in our development is that we only rely on coinductive program equivalences, bypassing the need to introduce term approximants, which were used in previous works characterizing type equivalence. The crucial part of this characterization is to show that type equivalent terms are normal form bisimilar: we do so by constructing shape typings that can only type terms of a specific normal form structure. Shape typings are a light form of principal types, a technique often used in intersection types to generate from one or few principal typing all possible typings of a term.
Cite as

Adrienne Lancelot. Separating Terms by Means of Multi Types, Coinductively. In 30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 4:1-4:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lancelot:LIPIcs.TYPES.2024.4,
  author =	{Lancelot, Adrienne},
  title =	{{Separating Terms by Means of Multi Types, Coinductively}},
  booktitle =	{30th International Conference on Types for Proofs and Programs (TYPES 2024)},
  pages =	{4:1--4:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-376-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{336},
  editor =	{M{\o}gelberg, Rasmus Ejlers and van den Berg, Benno},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.4},
  URN =		{urn:nbn:de:0030-drops-233660},
  doi =		{10.4230/LIPIcs.TYPES.2024.4},
  annote =	{Keywords: lambda calculus, intersection types, program equivalence}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.32
Compositional Static Value Analysis for Higher-Order Numerical Programs

Authors: Milla Valnet, Raphaël Monat, and Antoine Miné

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
Static analyzers have been successfully developed to detect runtime errors in many languages. However, the automatic analysis of functional languages remains a challenge due to their recursive functions, recursive algebraic data types, and higher-order functions. Classic type systems provide compositional methods that are in general not precise enough to prove the absence of runtime errors such as assertion failures. At the other end of the spectrum, deductive methods are more expressive but may require user guidance to prove invariants. Our work describes a static value analysis by abstract interpretation for a higher-order pure functional language. This analysis provides a sound and automatic approach to discover invariants and prevent assertion and match failures. We have designed a compositional analysis: functions are analyzed only once, at their definition site, generating a summary of their behavior. The summaries can be viewed as input-output relations expressed with relational abstract domains. We present two new abstract domains. A first abstract domain summarizes recursive algebraic data types. A second abstract domain lifts existing disjunctive relational summaries to higher-order by formalizing them as domains able to abstract higher-order functions. Both abstractions are parameterized by the abstractions of basic types (strings, integers, ...). Thanks to this parametric nature, both domains can be combined, allowing the analysis of higher-order functions manipulating algebraic data types and, conversely, algebraic data types using functions as first-class values. We have implemented this analysis in the open-source MOPSA platform. Preliminary evaluation confirms the precision of our approach on a set of 40 handwritten toy programs as well as 20 programs from the state-of-the-art Salto analyzer benchmark.
Cite as

Milla Valnet, Raphaël Monat, and Antoine Miné. Compositional Static Value Analysis for Higher-Order Numerical Programs. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 32:1-32:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{valnet_et_al:LIPIcs.ECOOP.2025.32,
  author =	{Valnet, Milla and Monat, Rapha\"{e}l and Min\'{e}, Antoine},
  title =	{{Compositional Static Value Analysis for Higher-Order Numerical Programs}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{32:1--32:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.32},
  URN =		{urn:nbn:de:0030-drops-233249},
  doi =		{10.4230/LIPIcs.ECOOP.2025.32},
  annote =	{Keywords: Static Value Analysis, Functional Programming, Abstract Interpretation}
}
Document
DOI: 10.4230/LIPIcs.STACS.2025.55
Modal Separation of Fixpoint Formulae

Authors: Jean Christoph Jung and Jędrzej Kołodziejski

Published in: LIPIcs, Volume 327, 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)

Abstract
Modal separability for modal fixpoint formulae is the problem to decide for two given modal fixpoint formulae φ,φ' whether there is a modal formula ψ that separates them, in the sense that φ ⊧ ψ and ψ ⊧ ¬φ'. We study modal separability and its special case modal definability over various classes of models, such as arbitrary models, finite models, trees, and models of bounded outdegree. Our main results are that modal separability is PSpace-complete over words, that is, models of outdegree ≤ 1, ExpTime-complete over unrestricted and over binary models, and 2-ExpTime-complete over models of outdegree bounded by some d ≥ 3. Interestingly, this latter case behaves fundamentally different from the other cases also in that modal logic does not enjoy the Craig interpolation property over this class. Motivated by this we study also the induced interpolant existence problem as a special case of modal separability, and show that it is coNExpTime-complete and thus harder than validity in the logic. Besides deciding separability, we also investigate the problem of efficient construction of separators. Finally, we consider in a case study the extension of modal fixpoint formulae by graded modalities and investigate separability by modal formulae and graded modal formulae.
Cite as

Jean Christoph Jung and Jędrzej Kołodziejski. Modal Separation of Fixpoint Formulae. In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 55:1-55:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{jung_et_al:LIPIcs.STACS.2025.55,
  author =	{Jung, Jean Christoph and Ko{\l}odziejski, J\k{e}drzej},
  title =	{{Modal Separation of Fixpoint Formulae}},
  booktitle =	{42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)},
  pages =	{55:1--55:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-365-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{327},
  editor =	{Beyersdorff, Olaf and Pilipczuk, Micha{\l} and Pimentel, Elaine and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2025.55},
  URN =		{urn:nbn:de:0030-drops-228804},
  doi =		{10.4230/LIPIcs.STACS.2025.55},
  annote =	{Keywords: Modal Logic, Fixpoint Logic, Separability, Interpolation}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.31
Simple Types for Probabilistic Termination

Authors: Willem Heijltjes and Georgina Majury

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
We present a new typing discipline to guarantee the probability of termination in probabilistic lambda-calculi. The main contribution is a particular naturality and simplicity: our probabilistic types are as simple types, but generated from probabilities as base types, representing a least probability of termination. Simple types are recovered by restricting probabilities to one. Our vehicle is the Probabilistic Event Lambda-Calculus by Dal Lago, Guerrieri, and Heijltjes, which presents a solution to the issue of confluence in probabilistic lambda-calculi. Our probabilistic type system provides an alternative solution to that using counting quantifiers by Antonelli, Dal Lago, and Pistone, for the same calculus. The problem that both type systems address is to give a lower bound on the probability that terms head-normalize. Following the recent Functional Machine Calculus by Heijltjes, our development takes the (simplified) Krivine machine as primary, and proceeds via an extension of the calculus with sequential composition and identity on the machine. Our type system then gives a natural account of termination probability on the Krivine machine, reflected back onto head-normalization for the original calculus. In this way we are able to avoid the use of counting quantifiers, while improving on the termination bounds given by Antonelli, Dal Lago, and Pistone.
Cite as

Willem Heijltjes and Georgina Majury. Simple Types for Probabilistic Termination. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 31:1-31:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{heijltjes_et_al:LIPIcs.CSL.2025.31,
  author =	{Heijltjes, Willem and Majury, Georgina},
  title =	{{Simple Types for Probabilistic Termination}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{31:1--31:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.31},
  URN =		{urn:nbn:de:0030-drops-227885},
  doi =		{10.4230/LIPIcs.CSL.2025.31},
  annote =	{Keywords: lambda-calculus, probabilistic termination, simple types}
}
Document
Position
DOI: 10.4230/TGDK.2.1.2
Grounding Stream Reasoning Research

Authors: Pieter Bonte, Jean-Paul Calbimonte, Daniel de Leng, Daniele Dell'Aglio, Emanuele Della Valle, Thomas Eiter, Federico Giannini, Fredrik Heintz, Konstantin Schekotihin, Danh Le-Phuoc, Alessandra Mileo, Patrik Schneider, Riccardo Tommasini, Jacopo Urbani, and Giacomo Ziffer

Published in: TGDK, Volume 2, Issue 1 (2024): Special Issue on Trends in Graph Data and Knowledge - Part 2. Transactions on Graph Data and Knowledge, Volume 2, Issue 1

Abstract
In the last decade, there has been a growing interest in applying AI technologies to implement complex data analytics over data streams. To this end, researchers in various fields have been organising a yearly event called the "Stream Reasoning Workshop" to share perspectives, challenges, and experiences around this topic. In this paper, the previous organisers of the workshops and other community members provide a summary of the main research results that have been discussed during the first six editions of the event. These results can be categorised into four main research areas: The first is concerned with the technological challenges related to handling large data streams. The second area aims at adapting and extending existing semantic technologies to data streams. The third and fourth areas focus on how to implement reasoning techniques, either considering deductive or inductive techniques, to extract new and valuable knowledge from the data in the stream. This summary is written not only to provide a crystallisation of the field, but also to point out distinctive traits of the stream reasoning community. Moreover, it also provides a foundation for future research by enumerating a list of use cases and open challenges, to stimulate others to join this exciting research area.
Cite as

Pieter Bonte, Jean-Paul Calbimonte, Daniel de Leng, Daniele Dell'Aglio, Emanuele Della Valle, Thomas Eiter, Federico Giannini, Fredrik Heintz, Konstantin Schekotihin, Danh Le-Phuoc, Alessandra Mileo, Patrik Schneider, Riccardo Tommasini, Jacopo Urbani, and Giacomo Ziffer. Grounding Stream Reasoning Research. In Special Issue on Trends in Graph Data and Knowledge - Part 2. Transactions on Graph Data and Knowledge (TGDK), Volume 2, Issue 1, pp. 2:1-2:47, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{bonte_et_al:TGDK.2.1.2,
  author =	{Bonte, Pieter and Calbimonte, Jean-Paul and de Leng, Daniel and Dell'Aglio, Daniele and Della Valle, Emanuele and Eiter, Thomas and Giannini, Federico and Heintz, Fredrik and Schekotihin, Konstantin and Le-Phuoc, Danh and Mileo, Alessandra and Schneider, Patrik and Tommasini, Riccardo and Urbani, Jacopo and Ziffer, Giacomo},
  title =	{{Grounding Stream Reasoning Research}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{2:1--2:47},
  ISSN =	{2942-7517},
  year =	{2024},
  volume =	{2},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.2.1.2},
  URN =		{urn:nbn:de:0030-drops-198597},
  doi =		{10.4230/TGDK.2.1.2},
  annote =	{Keywords: Stream Reasoning, Stream Processing, RDF streams, Streaming Linked Data, Continuous query processing, Temporal Logics, High-performance computing, Databases}
}
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.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.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.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.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.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}
}
  • Refine by Type
  • 53 Document/PDF
  • 9 Document/HTML
  • 1 Volume

  • Refine by Publication Year
  • 1 2026
  • 7 2025
  • 1 2024
  • 40 2018
  • 2 2017
  • Show More...

  • Refine by Author
  • 7 Jung, Achim
  • 3 Das, Anupam
  • 2 Ahrens, Benedikt
  • 2 Clairambault, Pierre
  • 2 Dawar, Anuj
  • Show More...

  • Refine by Series/Journal
  • 49 LIPIcs
  • 1 TGDK
  • 1 DagRep
  • 1 DagSemRep
  • 1 DagSemProc

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

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

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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