Volume
LIPIcs, Volume 152
28th EACSL Annual Conference on Computer Science Logic (CSL 2020)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL)
Event
CSL 2020, January 13-16, 2020, Barcelona, SpainEditors
Publication Details
- published at: 2020-01-06
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-132-0
- DBLP: db/conf/csl/csl2020
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 152, CSL'20, Complete Volume
Abstract
LIPIcs, Volume 152, CSL'20, Complete Volume
Cite as
28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@Proceedings{fernandez_et_al:LIPIcs.CSL.2020,
title = {{LIPIcs, Volume 152, CSL'20, Complete Volume}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020},
URN = {urn:nbn:de:0030-drops-117841},
doi = {10.4230/LIPIcs.CSL.2020},
annote = {Keywords: Theory of computation, Logic}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 0:i-0:xviii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{fernandez_et_al:LIPIcs.CSL.2020.0,
author = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {0:i--0:xviii},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.0},
URN = {urn:nbn:de:0030-drops-116431},
doi = {10.4230/LIPIcs.CSL.2020.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
Verification of Security Protocols (Invited Talk)
Abstract
Cryptographic protocols aim at securing communications over insecure networks like the Internet. Over the past decades, numerous decision procedures and tools have been developed to automatically analyse the security of protocols. The field has now reached a good level of maturity with efficient techniques for the automatic security analysis of protocols
After an overview of some famous protocols and flaws, we will describe the current techniques for security protocols analysis, often based on logic, and review the key challenges towards a fully automated verification.
Cite as
Véronique Cortier. Verification of Security Protocols (Invited Talk). In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{cortier:LIPIcs.CSL.2020.1,
author = {Cortier, V\'{e}ronique},
title = {{Verification of Security Protocols}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {1:1--1:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.1},
URN = {urn:nbn:de:0030-drops-116447},
doi = {10.4230/LIPIcs.CSL.2020.1},
annote = {Keywords: Security protocols, automated deduction, security}
}
Document
Invited Talk
Symmetric Computation (Invited Talk)
Abstract
We discuss a recent convergence of notions of symmetric computation arising in the theory of linear programming, in logic and in circuit complexity. This leads us to a coherent and robust definition of problems that are efficiently and symmetrically solvable. This is at once a rich class of problems and one for which we have methods for proving lower bounds. In this paper, we take a tour through results which show applications of these methods in a number of areas.
Cite as
Anuj Dawar. Symmetric Computation (Invited Talk). In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 2:1-2:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{dawar:LIPIcs.CSL.2020.2,
author = {Dawar, Anuj},
title = {{Symmetric Computation}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {2:1--2:12},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.2},
URN = {urn:nbn:de:0030-drops-116455},
doi = {10.4230/LIPIcs.CSL.2020.2},
annote = {Keywords: Descriptive Complexity, Fixed-point Logic with Counting, Circuit Complexity, Linear Programming, Hardness of Approximation, Arithmetic Circuits}
}
Document
Invited Talk
Solving Word Equations (And Other Unification Problems) by Recompression (Invited Talk)
Abstract
In word equation problem we are given an equation u = v, where both u and v are words of letters and variables, and ask for a substitution of variables by words that equalizes the sides of the equation. This problem was first solved by Makanin and a different solution was proposed by Plandowski only 20 years later, his solution works in PSPACE, which is the best computational complexity bound known for this problem; on the other hand, the only known lower-bound is NP-hardness. In both cases the algorithms (and proofs) employed nontrivial facts on word combinatorics.
In the paper I will present an application of a recent technique of recompression, which simplifies the known proofs and (slightly) lowers the complexity to linear nondeterministic space. The technique is based on employing simple compression rules (replacement of two letters ab by a new letter c, replacement of maximal repetitions of a by a new letter), and modifying the equations (replacing a variable X by bX or Xa) so that those operations are sound and complete. In particular, no combinatorial properties of strings are used.
The approach turns out to be quite robust and can be applied to various generalizations and related scenarios (context unification, i.e. equations over terms; equations over traces, i.e. partially ordered words; ...).
Cite as
Artur Jeż. Solving Word Equations (And Other Unification Problems) by Recompression (Invited Talk). In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 3:1-3:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{jez:LIPIcs.CSL.2020.3,
author = {Je\.{z}, Artur},
title = {{Solving Word Equations (And Other Unification Problems) by Recompression}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {3:1--3:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.3},
URN = {urn:nbn:de:0030-drops-116468},
doi = {10.4230/LIPIcs.CSL.2020.3},
annote = {Keywords: word equation, context unification, equations in groups, compression}
}
Document
Invited Talk
Strong Bisimulation for Control Operators (Invited Talk)
Abstract
The purpose of this paper is to identify programs with control operators whose reduction semantics are in exact correspondence. This is achieved by introducing a relation ≃, defined over a revised presentation of Parigot’s λμ-calculus we dub ΛM.
Our result builds on two fundamental ingredients: (1) factorization of λμ-reduction into multiplicative and exponential steps by means of explicit term operators of ΛM, and (2) translation of ΛM-terms into Laurent’s polarized proof-nets (PPN) such that cut-elimination in PPN simulates our calculus. Our proposed relation ≃ is shown to characterize structural equivalence in PPN. Most notably, ≃ is shown to be a strong bisimulation with respect to reduction in ΛM, i.e. two ≃-equivalent terms have the exact same reduction semantics, a result which fails for Regnier’s σ-equivalence in λ-calculus as well as for Laurent’s σ-equivalence in λμ.
Cite as
Delia Kesner, Eduardo Bonelli, and Andrés Viso. Strong Bisimulation for Control Operators (Invited Talk). In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 4:1-4:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{kesner_et_al:LIPIcs.CSL.2020.4,
author = {Kesner, Delia and Bonelli, Eduardo and Viso, Andr\'{e}s},
title = {{Strong Bisimulation for Control Operators}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {4:1--4:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.4},
URN = {urn:nbn:de:0030-drops-116473},
doi = {10.4230/LIPIcs.CSL.2020.4},
annote = {Keywords: Lambda-mu calculus, proof-nets, strong bisimulation}
}
Document
Invited Talk
From Classical Proof Theory to P versus NP: a Guide to Bounded Theories (Invited Talk)
Abstract
This talk explores the question of what does logic and specifically proof theory can tell us about the fundamental hardness questions in computational complexity. We start with a brief description of the main concepts behind bounded arithmetic which is a family of weak formal theories of arithmetic that mirror in a precise manner the world of propositional proofs: if a statement of a given form is provable in a given bounded arithmetic theory then the same statement is suitably translated to a family of propositional formulas with short (polynomial-size) proofs in a corresponding propositional proof system.
We will proceed to describe the motivations behind the study of bounded arithmetic theories, their corresponding propositional proof systems, and how they relate to the fundamental complexity class separations and circuit lower bounds questions in computational complexity. We provide a collage of results and recent developments showing how bounded arithmetic and propositional proof complexity form a cohesive framework in which both concrete combinatorial questions about complexity as well as meta-mathematical questions about provability of statements of complexity theory itself, are studied.
Specific topics we shall mention are: (i) The bounded reverse mathematics program [Stephen Cook and Phuong Nguyen, 2010]: studying the weakest possible axiomatic assumptions that can prove important results in mathematics and computing (cf. [Iddo Tzameret and Stephen A. Cook, 2017; Pavel Hrubeš and Iddo Tzameret, 2015]), and the correspondence between circuit classes and theories. (ii) The meta-mathematics of computational complexity: what kind of reasoning power do we need in order to prove major results in complexity theory itself, and applications to complexity lower bounds (cf. [Razborov, 1995; Rahul Santhanam and Jan Pich, 2019]). (iii) Proof complexity: the systematic treatment of propositional proofs as combinatorial and algebraic objects and their algorithmic applications (cf. [Samuel Buss, 2012; Tonnian Pitassi and Iddo Tzameret, 2016; Noah Fleming et al., 2019]).
Cite as
Iddo Tzameret. From Classical Proof Theory to P versus NP: a Guide to Bounded Theories (Invited Talk). In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 5:1-5:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{tzameret:LIPIcs.CSL.2020.5,
author = {Tzameret, Iddo},
title = {{From Classical Proof Theory to P versus NP: a Guide to Bounded Theories}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {5:1--5:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.5},
URN = {urn:nbn:de:0030-drops-116482},
doi = {10.4230/LIPIcs.CSL.2020.5},
annote = {Keywords: Bounded arithmetic, complexity class separations, circuit complexity, proof complexity, weak theories of arithmetic, feasible mathematics}
}
Document
Generalized Connectives for Multiplicative Linear Logic
Abstract
In this paper we investigate the notion of generalized connective for multiplicative linear logic. We introduce a notion of orthogonality for partitions of a finite set and we study the family of connectives which can be described by two orthogonal sets of partitions.
We prove that there is a special class of connectives that can never be decomposed by means of the multiplicative conjunction ⊗ and disjunction ⅋, providing an infinite family of non-decomposable connectives, called Girard connectives. We show that each Girard connective can be naturally described by a type (a set of partitions equal to its double-orthogonal) and its orthogonal type. In addition, one of these two types is the union of the types associated to a family of MLL-formulas in disjunctive normal form, and these formulas only differ for the cyclic permutations of their atoms.
Cite as
Matteo Acclavio and Roberto Maieli. Generalized Connectives for Multiplicative Linear Logic. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 6:1-6:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{acclavio_et_al:LIPIcs.CSL.2020.6,
author = {Acclavio, Matteo and Maieli, Roberto},
title = {{Generalized Connectives for Multiplicative Linear Logic}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {6:1--6:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.6},
URN = {urn:nbn:de:0030-drops-116490},
doi = {10.4230/LIPIcs.CSL.2020.6},
annote = {Keywords: Linear Logic, Partitions Sets, Proof Nets, Sequent Calculus}
}
Document
On Free Completely Iterative Algebras
Abstract
For every finitary set functor F we demonstrate that free algebras carry a canonical partial order. In case F is bicontinuous, we prove that the cpo obtained as the conservative completion of the free algebra is the free completely iterative algebra. Moreover, the algebra structure of the latter is the unique continuous extension of the algebra structure of the free algebra.
For general finitary functors the free algebra and the free completely iterative algebra are proved to be posets sharing the same conservative completion. And for every recursive equation in the free completely iterative algebra the solution is obtained as the join of an ω-chain of approximate solutions in the free algebra.
Cite as
Jiří Adámek. On Free Completely Iterative Algebras. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 7:1-7:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{adamek:LIPIcs.CSL.2020.7,
author = {Ad\'{a}mek, Ji\v{r}{\'\i}},
title = {{On Free Completely Iterative Algebras}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {7:1--7:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.7},
URN = {urn:nbn:de:0030-drops-116503},
doi = {10.4230/LIPIcs.CSL.2020.7},
annote = {Keywords: free algebra, completely iterative algebra, terminal coalgebra, initial algebra, finitary functor}
}
Document
Strongly Unambiguous Büchi Automata Are Polynomially Predictable With Membership Queries
Abstract
A Büchi automaton is strongly unambiguous if every word w ∈ Σ^ω has at most one final path. Many properties of strongly unambiguous Büchi automata (SUBAs) are known. They are fully expressive: every regular ω-language can be represented by a SUBA. Equivalence and containment of SUBAs can be decided in polynomial time. SUBAs may be exponentially smaller than deterministic Muller automata and may be exponentially bigger than deterministic Büchi automata. In this work we show that SUBAs can be learned in polynomial time using membership and certain non-proper equivalence queries, which implies that they are polynomially predictable with membership queries. In contrast, under plausible cryptographic assumptions, non-deterministic Büchi automata are not polynomially predictable with membership queries.
Cite as
Dana Angluin, Timos Antonopoulos, and Dana Fisman. Strongly Unambiguous Büchi Automata Are Polynomially Predictable With Membership Queries. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{angluin_et_al:LIPIcs.CSL.2020.8,
author = {Angluin, Dana and Antonopoulos, Timos and Fisman, Dana},
title = {{Strongly Unambiguous B\"{u}chi Automata Are Polynomially Predictable With Membership Queries}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {8:1--8:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.8},
URN = {urn:nbn:de:0030-drops-116519},
doi = {10.4230/LIPIcs.CSL.2020.8},
annote = {Keywords: Polynomially predictable languages, Automata learning, Strongly unambiguous B\"{u}chi automata, Automata succinctness, Regular \omega-languages, Grammatical inference}
}
Document
A Robust Class of Linear Recurrence Sequences
Abstract
We introduce a subclass of linear recurrence sequences which we call poly-rational sequences because they are denoted by rational expressions closed under sum and product. We show that this class is robust by giving several characterisations: polynomially ambiguous weighted automata, copyless cost-register automata, rational formal series, and linear recurrence sequences whose eigenvalues are roots of rational numbers.
Cite as
Corentin Barloy, Nathanaël Fijalkow, Nathan Lhote, and Filip Mazowiecki. A Robust Class of Linear Recurrence Sequences. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 9:1-9:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{barloy_et_al:LIPIcs.CSL.2020.9,
author = {Barloy, Corentin and Fijalkow, Nathana\"{e}l and Lhote, Nathan and Mazowiecki, Filip},
title = {{A Robust Class of Linear Recurrence Sequences}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {9:1--9:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.9},
URN = {urn:nbn:de:0030-drops-116521},
doi = {10.4230/LIPIcs.CSL.2020.9},
annote = {Keywords: linear recurrence sequences, weighted automata, cost-register automata}
}
Document
Coverage and Vacuity in Network Formation Games
Abstract
The frameworks of coverage and vacuity in formal verification analyze the effect of mutations applied to systems or their specifications. We adopt these notions to network formation games, analyzing the effect of a change in the cost of a resource. We consider two measures to be affected: the cost of the Social Optimum and extremums of costs of Nash Equilibria. Our results offer a formal framework to the effect of mutations in network formation games and include a complexity analysis of related decision problems. They also tighten the relation between algorithmic game theory and formal verification, suggesting refined definitions of coverage and vacuity for the latter.
Cite as
Gili Bielous and Orna Kupferman. Coverage and Vacuity in Network Formation Games. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{bielous_et_al:LIPIcs.CSL.2020.10,
author = {Bielous, Gili and Kupferman, Orna},
title = {{Coverage and Vacuity in Network Formation Games}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {10:1--10:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.10},
URN = {urn:nbn:de:0030-drops-116532},
doi = {10.4230/LIPIcs.CSL.2020.10},
annote = {Keywords: Network Formation Games, Vacuity, Coverage}
}
Document
A Complete Axiomatisation of a Fragment of Language Algebra
Abstract
We consider algebras of languages over the signature of reversible Kleene lattices, that is the regular operations (empty and unit languages, union, concatenation and Kleene star) together with intersection and mirror image. We provide a complete set of axioms for the equational theory of these algebras. This proof was developed in the proof assistant Coq.
Cite as
Paul Brunet. A Complete Axiomatisation of a Fragment of Language Algebra. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 11:1-11:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{brunet:LIPIcs.CSL.2020.11,
author = {Brunet, Paul},
title = {{A Complete Axiomatisation of a Fragment of Language Algebra}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {11:1--11:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.11},
URN = {urn:nbn:de:0030-drops-116546},
doi = {10.4230/LIPIcs.CSL.2020.11},
annote = {Keywords: Kleene algebra, language algebra, completeness theorem, axiomatisation}
}
Document
Proof Complexity of Systems of (Non-Deterministic) Decision Trees and Branching Programs
Abstract
This paper studies propositional proof systems in which lines are sequents of decision trees or branching programs, deterministic or non-deterministic. Decision trees (DTs) are represented by a natural term syntax, inducing the system LDT, and non-determinism is modelled by including disjunction, ∨, as primitive (system LNDT). Branching programs generalise DTs to dag-like structures and are duly handled by extension variables in our setting, as is common in proof complexity (systems eLDT and eLNDT).
Deterministic and non-deterministic branching programs are natural nonuniform analogues of log-space (L) and nondeterministic log-space (NL), respectively. Thus eLDT and eLNDT serve as natural systems of reasoning corresponding to L and NL, respectively.
The main results of the paper are simulation and non-simulation results for tree-like and dag-like proofs in LDT, LNDT, eLDT and eLNDT. We also compare them with Frege systems, constant-depth Frege systems and extended Frege systems.
Cite as
Sam Buss, Anupam Das, and Alexander Knop. Proof Complexity of Systems of (Non-Deterministic) Decision Trees and Branching Programs. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{buss_et_al:LIPIcs.CSL.2020.12,
author = {Buss, Sam and Das, Anupam and Knop, Alexander},
title = {{Proof Complexity of Systems of (Non-Deterministic) Decision Trees and Branching Programs}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {12:1--12:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.12},
URN = {urn:nbn:de:0030-drops-116553},
doi = {10.4230/LIPIcs.CSL.2020.12},
annote = {Keywords: proof complexity, decision trees, branching programs, logspace, sequent calculus, non-determinism, low-depth complexity}
}
Document
Internal Parametricity for Cubical Type Theory
Abstract
We define a computational type theory combining the contentful equality structure of cartesian cubical type theory with internal parametricity primitives. The combined theory supports both univalence and its relational equivalent, which we call relativity. We demonstrate the use of the theory by analyzing polymorphic functions between higher inductive types, and we give an account of the identity extension lemma for internal parametricity.
Cite as
Evan Cavallo and Robert Harper. Internal Parametricity for Cubical Type Theory. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{cavallo_et_al:LIPIcs.CSL.2020.13,
author = {Cavallo, Evan and Harper, Robert},
title = {{Internal Parametricity for Cubical Type Theory}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {13:1--13:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.13},
URN = {urn:nbn:de:0030-drops-116564},
doi = {10.4230/LIPIcs.CSL.2020.13},
annote = {Keywords: parametricity, cubical type theory, higher inductive types}
}
Document
Unifying Cubical Models of Univalent Type Theory
Abstract
We present a new constructive model of univalent type theory based on cubical sets. Unlike prior work on cubical models, ours depends neither on diagonal cofibrations nor connections. This is made possible by weakening the notion of fibration from the cartesian cubical set model, so that it is not necessary to assume that the diagonal on the interval is a cofibration. We have formally verified in Agda that these fibrations are closed under the type formers of cubical type theory and that the model satisfies the univalence axiom. By applying the construction in the presence of diagonal cofibrations or connections and reversals, we recover the existing cartesian and De Morgan cubical set models as special cases. Generalizing earlier work of Sattler for cubical sets with connections, we also obtain a Quillen model structure.
Cite as
Evan Cavallo, Anders Mörtberg, and Andrew W Swan. Unifying Cubical Models of Univalent Type Theory. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{cavallo_et_al:LIPIcs.CSL.2020.14,
author = {Cavallo, Evan and M\"{o}rtberg, Anders and Swan, Andrew W},
title = {{Unifying Cubical Models of Univalent Type Theory}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {14:1--14:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.14},
URN = {urn:nbn:de:0030-drops-116578},
doi = {10.4230/LIPIcs.CSL.2020.14},
annote = {Keywords: Cubical Set Models, Cubical Type Theory, Homotopy Type Theory, Univalent Foundations}
}
Document
FO-Definability of Shrub-Depth
Abstract
Shrub-depth is a graph invariant often considered as an extension of tree-depth to dense graphs. We show that the model-checking problem of monadic second-order logic on a class of graphs of bounded shrub-depth can be decided by AC^0-circuits after a precomputation on the formula. This generalizes a similar result on graphs of bounded tree-depth [Y. Chen and J. Flum, 2018]. At the core of our proof is the definability in first-order logic of tree-models for graphs of bounded shrub-depth.
Cite as
Yijia Chen and Jörg Flum. FO-Definability of Shrub-Depth. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{chen_et_al:LIPIcs.CSL.2020.15,
author = {Chen, Yijia and Flum, J\"{o}rg},
title = {{FO-Definability of Shrub-Depth}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {15:1--15:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.15},
URN = {urn:nbn:de:0030-drops-116587},
doi = {10.4230/LIPIcs.CSL.2020.15},
annote = {Keywords: shrub-depth, model-checking, monadic second-order logic}
}
Document
Taylor expansion for Call-By-Push-Value
Abstract
The connection between the Call-By-Push-Value lambda-calculus introduced by Levy and Linear Logic introduced by Girard has been widely explored through a denotational view reflecting the precise ruling of resources in this language. We take a further step in this direction and apply Taylor expansion introduced by Ehrhard and Regnier. We define a resource lambda-calculus in whose terms can be used to approximate terms of Call-By-Push-Value. We show that this approximation is coherent with reduction and with the translations of Call-By-Name and Call-By-Value strategies into Call-By-Push-Value.
Cite as
Jules Chouquet and Christine Tasson. Taylor expansion for Call-By-Push-Value. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 16:1-16:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{chouquet_et_al:LIPIcs.CSL.2020.16,
author = {Chouquet, Jules and Tasson, Christine},
title = {{Taylor expansion for Call-By-Push-Value}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {16:1--16:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.16},
URN = {urn:nbn:de:0030-drops-116594},
doi = {10.4230/LIPIcs.CSL.2020.16},
annote = {Keywords: Call-By-Push-Value, Quantitative semantics, Taylor expansion, Linear Logic}
}
Document
Tangent Categories from the Coalgebras of Differential Categories
Abstract
Following the pattern from linear logic, the coKleisli category of a differential category is a Cartesian differential category. What then is the coEilenberg-Moore category of a differential category? The answer is a tangent category! A key example arises from the opposite of the category of Abelian groups with the free exponential modality. The coEilenberg-Moore category, in this case, is the opposite of the category of commutative rings. That the latter is a tangent category captures a fundamental aspect of both algebraic geometry and Synthetic Differential Geometry. The general result applies when there are no negatives and thus encompasses examples arising from combinatorics and computer science.
Cite as
Robin Cockett, Jean-Simon Pacaud Lemay, and Rory B. B. Lucyshyn-Wright. Tangent Categories from the Coalgebras of Differential Categories. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 17:1-17:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{cockett_et_al:LIPIcs.CSL.2020.17,
author = {Cockett, Robin and Lemay, Jean-Simon Pacaud and Lucyshyn-Wright, Rory B. B.},
title = {{Tangent Categories from the Coalgebras of Differential Categories}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {17:1--17:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.17},
URN = {urn:nbn:de:0030-drops-116607},
doi = {10.4230/LIPIcs.CSL.2020.17},
annote = {Keywords: Differential categories, Tangent categories, Coalgebra Modalities}
}
Document
Reverse Derivative Categories
Abstract
The reverse derivative is a fundamental operation in machine learning and automatic differentiation [Martín Abadi et al., 2015; Griewank, 2012]. This paper gives a direct axiomatization of a category with a reverse derivative operation, in a similar style to that given by [Blute et al., 2009] for a forward derivative. Intriguingly, a category with a reverse derivative also has a forward derivative, but the converse is not true. In fact, we show explicitly what a forward derivative is missing: a reverse derivative is equivalent to a forward derivative with a dagger structure on its subcategory of linear maps. Furthermore, we show that these linear maps form an additively enriched category with dagger biproducts.
Cite as
Robin Cockett, Geoffrey Cruttwell, Jonathan Gallagher, Jean-Simon Pacaud Lemay, Benjamin MacAdam, Gordon Plotkin, and Dorette Pronk. Reverse Derivative Categories. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 18:1-18:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{cockett_et_al:LIPIcs.CSL.2020.18,
author = {Cockett, Robin and Cruttwell, Geoffrey and Gallagher, Jonathan and Lemay, Jean-Simon Pacaud and MacAdam, Benjamin and Plotkin, Gordon and Pronk, Dorette},
title = {{Reverse Derivative Categories}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {18:1--18:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.18},
URN = {urn:nbn:de:0030-drops-116611},
doi = {10.4230/LIPIcs.CSL.2020.18},
annote = {Keywords: Reverse Derivatives, Cartesian Reverse Differential Categories, Categorical Semantics, Cartesian Differential Categories, Dagger Categories, Automatic Differentiation}
}
Document
Internal Calculi for Separation Logics
Abstract
We present a general approach to axiomatise separation logics with heaplet semantics with no external features such as nominals/labels. To start with, we design the first (internal) Hilbert-style axiomatisation for the quantifier-free separation logic SL(∗, -*). We instantiate the method by introducing a new separation logic with essential features: it is equipped with the separating conjunction, the predicate ls, and a natural guarded form of first-order quantification. We apply our approach for its axiomatisation. As a by-product of our method, we also establish the exact expressive power of this new logic and we show PSpace-completeness of its satisfiability problem.
Cite as
Stéphane Demri, Etienne Lozes, and Alessio Mansutti. Internal Calculi for Separation Logics. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 19:1-19:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{demri_et_al:LIPIcs.CSL.2020.19,
author = {Demri, St\'{e}phane and Lozes, Etienne and Mansutti, Alessio},
title = {{Internal Calculi for Separation Logics}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {19:1--19:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.19},
URN = {urn:nbn:de:0030-drops-116625},
doi = {10.4230/LIPIcs.CSL.2020.19},
annote = {Keywords: Separation logic, internal calculus, adjunct/quantifier elimination}
}
Document
Monitoring Event Frequencies
Abstract
The monitoring of event frequencies can be used to recognize behavioral anomalies, to identify trends, and to deduce or discard hypotheses about the underlying system. For example, the performance of a web server may be monitored based on the ratio of the total count of requests from the least and most active clients. Exact frequency monitoring, however, can be prohibitively expensive; in the above example it would require as many counters as there are clients. In this paper, we propose the efficient probabilistic monitoring of common frequency properties, including the mode (i.e., the most common event) and the median of an event sequence. We define a logic to express composite frequency properties as a combination of atomic frequency properties. Our main contribution is an algorithm that, under suitable probabilistic assumptions, can be used to monitor these important frequency properties with four counters, independent of the number of different events. Our algorithm samples longer and longer subwords of an infinite event sequence. We prove the almost-sure convergence of our algorithm by generalizing ergodic theory from increasing-length prefixes to increasing-length subwords of an infinite sequence. A similar algorithm could be used to learn a connected Markov chain of a given structure from observing its outputs, to arbitrary precision, for a given confidence.
Cite as
Thomas Ferrère, Thomas A. Henzinger, and Bernhard Kragl. Monitoring Event Frequencies. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 20:1-20:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{ferrere_et_al:LIPIcs.CSL.2020.20,
author = {Ferr\`{e}re, Thomas and Henzinger, Thomas A. and Kragl, Bernhard},
title = {{Monitoring Event Frequencies}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {20:1--20:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.20},
URN = {urn:nbn:de:0030-drops-116633},
doi = {10.4230/LIPIcs.CSL.2020.20},
annote = {Keywords: monitoring, frequency property, Markov chain}
}
Document
Automatic Equivalence Structures of Polynomial Growth
Abstract
In this paper we study the class EqP of automatic equivalence structures of the form ?=(D, E) where the domain D is a regular language of polynomial growth and E is an equivalence relation on D. Our goal is to investigate the following two foundational problems (in the theory of automatic structures) aimed for the class EqP. The first is to find algebraic characterizations of structures from EqP, and the second is to investigate the isomorphism problem for the class EqP. We provide full solutions to these two problems. First, we produce a characterization of structures from EqP through multivariate polynomials. Second, we present two contrasting results. On the one hand, we prove that the isomorphism problem for structures from the class EqP is undecidable. On the other hand, we prove that the isomorphism problem is decidable for structures from EqP with domains of quadratic growth.
Cite as
Moses Ganardi and Bakhadyr Khoussainov. Automatic Equivalence Structures of Polynomial Growth. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 21:1-21:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{ganardi_et_al:LIPIcs.CSL.2020.21,
author = {Ganardi, Moses and Khoussainov, Bakhadyr},
title = {{Automatic Equivalence Structures of Polynomial Growth}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {21:1--21:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.21},
URN = {urn:nbn:de:0030-drops-116645},
doi = {10.4230/LIPIcs.CSL.2020.21},
annote = {Keywords: automatic structures, polynomial growth, isomorphism problem}
}
Document
Guarded Teams: The Horizontally Guarded Case
Abstract
Team semantics admits reasoning about large sets of data, modelled by sets of assignments (called teams), with first-order syntax. This leads to high expressive power and complexity, particularly in the presence of atomic dependency properties for such data sets. It is therefore interesting to explore fragments and variants of logic with team semantics that permit model-theoretic tools and algorithmic methods to control this explosion in expressive power and complexity.
We combine here the study of team semantics with the notion of guarded logics, which are well-understood in the case of classical Tarski semantics, and known to strike a good balance between expressive power and algorithmic manageability. In fact there are two strains of guardedness for teams. Horizontal guardedness requires the individual assignments of the team to be guarded in the usual sense of guarded logics. Vertical guardedness, on the other hand, posits an additional (or definable) hypergraph structure on relational structures in order to interpret a constraint on the component-wise variability of assignments within teams.
In this paper we investigate the horizontally guarded case. We study horizontally guarded logics for teams and appropriate notions of guarded team bisimulation. In particular, we establish characterisation theorems that relate invariance under guarded team bisimulation with guarded team logics, but also with logics under classical Tarski semantics.
Cite as
Erich Grädel and Martin Otto. Guarded Teams: The Horizontally Guarded Case. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 22:1-22:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{gradel_et_al:LIPIcs.CSL.2020.22,
author = {Gr\"{a}del, Erich and Otto, Martin},
title = {{Guarded Teams: The Horizontally Guarded Case}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {22:1--22:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.22},
URN = {urn:nbn:de:0030-drops-116650},
doi = {10.4230/LIPIcs.CSL.2020.22},
annote = {Keywords: Team semantics, guarded logics, bisimulation, characterisation theorems}
}
Document
Order-Invariant First-Order Logic over Hollow Trees
Abstract
We show that the expressive power of order-invariant first-order logic collapses to first-order logic over hollow trees. A hollow tree is an unranked ordered tree where every non leaf node has at most four adjacent nodes: two siblings (left and right) and its first and last children. In particular there is no predicate for the linear order among siblings nor for the descendant relation. Moreover only the first and last nodes of a siblinghood are linked to their parent node, and the parent-child relation cannot be completely reconstructed in first-order.
Cite as
Julien Grange and Luc Segoufin. Order-Invariant First-Order Logic over Hollow Trees. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 23:1-23:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{grange_et_al:LIPIcs.CSL.2020.23,
author = {Grange, Julien and Segoufin, Luc},
title = {{Order-Invariant First-Order Logic over Hollow Trees}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {23:1--23:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.23},
URN = {urn:nbn:de:0030-drops-116661},
doi = {10.4230/LIPIcs.CSL.2020.23},
annote = {Keywords: order-invariance, first-order logic}
}
Document
Glueability of Resource Proof-Structures: Inverting the Taylor Expansion
Abstract
A Multiplicative-Exponential Linear Logic (MELL) proof-structure can be expanded into a set of resource proof-structures: its Taylor expansion. We introduce a new criterion characterizing those sets of resource proof-structures that are part of the Taylor expansion of some MELL proof-structure, through a rewriting system acting both on resource and MELL proof-structures.
Cite as
Giulio Guerrieri, Luc Pellissier, and Lorenzo Tortora de Falco. Glueability of Resource Proof-Structures: Inverting the Taylor Expansion. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 24:1-24:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{guerrieri_et_al:LIPIcs.CSL.2020.24,
author = {Guerrieri, Giulio and Pellissier, Luc and Tortora de Falco, Lorenzo},
title = {{Glueability of Resource Proof-Structures: Inverting the Taylor Expansion}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {24:1--24:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.24},
URN = {urn:nbn:de:0030-drops-116674},
doi = {10.4230/LIPIcs.CSL.2020.24},
annote = {Keywords: linear logic, Taylor expansion, proof-net, natural transformation}
}
Document
On the Union Closed Fragment of Existential Second-Order Logic and Logics with Team Semantics
Abstract
We present syntactic characterisations for the union closed fragments of existential second-order logic and of logics with team semantics. Since union closure is a semantical and undecidable property, the normal form we introduce enables the handling and provides a better understanding of this fragment. We also introduce inclusion-exclusion games that turn out to be precisely the corresponding model-checking games. These games are not only interesting in their own right, but they also are a key factor towards building a bridge between the semantic and syntactic fragments. On the level of logics with team semantics we additionally present restrictions of inclusion-exclusion logic to capture the union closed fragment. Moreover, we define a team based atom that when adding it to first-order logic also precisely captures the union closed fragment of existential second-order logic which answers an open question by Galliani and Hella.
Cite as
Matthias Hoelzel and Richard Wilke. On the Union Closed Fragment of Existential Second-Order Logic and Logics with Team Semantics. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 25:1-25:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{hoelzel_et_al:LIPIcs.CSL.2020.25,
author = {Hoelzel, Matthias and Wilke, Richard},
title = {{On the Union Closed Fragment of Existential Second-Order Logic and Logics with Team Semantics}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {25:1--25:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.25},
URN = {urn:nbn:de:0030-drops-116681},
doi = {10.4230/LIPIcs.CSL.2020.25},
annote = {Keywords: Higher order logic, Existential second-order logic, Team semantics, Closure properties, Union closure, Model-checking games, Syntactic charactisations of semantical fragments}
}
Document
Expressive Logics for Coinductive Predicates
Abstract
The classical Hennessy-Milner theorem says that two states of an image-finite transition system are bisimilar if and only if they satisfy the same formulas in a certain modal logic. In this paper we study this type of result in a general context, moving from transition systems to coalgebras and from bisimilarity to coinductive predicates. We formulate when a logic fully characterises a coinductive predicate on coalgebras, by providing suitable notions of adequacy and expressivity, and give sufficient conditions on the semantics. The approach is illustrated with logics characterising similarity, divergence and a behavioural metric on automata.
Cite as
Clemens Kupke and Jurriaan Rot. Expressive Logics for Coinductive Predicates. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{kupke_et_al:LIPIcs.CSL.2020.26,
author = {Kupke, Clemens and Rot, Jurriaan},
title = {{Expressive Logics for Coinductive Predicates}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {26:1--26:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.26},
URN = {urn:nbn:de:0030-drops-116698},
doi = {10.4230/LIPIcs.CSL.2020.26},
annote = {Keywords: Coalgebra, Fibration, Modal Logic}
}
Document
State Space Reduction For Parity Automata
Abstract
Exact minimization of ω-automata is a difficult problem and heuristic algorithms are a subject of current research. We propose several new approaches to reduce the state space of deterministic parity automata. These are based on extracting information from structures within the automaton, such as strongly connected components, coloring of the states, and equivalence classes of given relations, to determine states that can safely be merged. We also establish a framework to generalize the notion of quotient automata and uniformly describe such algorithms. The description of these procedures consists of a theoretical analysis as well as data collected from experiments.
Cite as
Christof Löding and Andreas Tollkötter. State Space Reduction For Parity Automata. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 27:1-27:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{loding_et_al:LIPIcs.CSL.2020.27,
author = {L\"{o}ding, Christof and Tollk\"{o}tter, Andreas},
title = {{State Space Reduction For Parity Automata}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {27:1--27:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.27},
URN = {urn:nbn:de:0030-drops-116701},
doi = {10.4230/LIPIcs.CSL.2020.27},
annote = {Keywords: automata, \omega-automata, parity, minimization, state space reduction, deterministic, simulation relations}
}
Document
Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents
Abstract
We provide a direct method for proving Craig interpolation for a range of modal and intuitionistic logics, including those containing a "converse" modality. We demonstrate this method for classical tense logic, its extensions with path axioms, and for bi-intuitionistic logic. These logics do not have straightforward formalisations in the traditional Gentzen-style sequent calculus, but have all been shown to have cut-free nested sequent calculi. The proof of the interpolation theorem uses these calculi and is purely syntactic, without resorting to embeddings, semantic arguments, or interpreted connectives external to the underlying logical language. A novel feature of our proof includes an orthogonality condition for defining duality between interpolants.
Cite as
Tim Lyon, Alwen Tiu, Rajeev Goré, and Ranald Clouston. Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 28:1-28:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{lyon_et_al:LIPIcs.CSL.2020.28,
author = {Lyon, Tim and Tiu, Alwen and Gor\'{e}, Rajeev and Clouston, Ranald},
title = {{Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {28:1--28:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.28},
URN = {urn:nbn:de:0030-drops-116713},
doi = {10.4230/LIPIcs.CSL.2020.28},
annote = {Keywords: Bi-intuitionistic logic, Interpolation, Nested calculi, Proof theory, Sequents, Tense logics}
}
Document
The Keys to Decidable HyperLTL Satisfiability: Small Models or Very Simple Formulas
Abstract
HyperLTL, the extension of Linear Temporal Logic by trace quantifiers, is a uniform framework for expressing information flow policies by relating multiple traces of a security-critical system. HyperLTL has been successfully applied to express fundamental security policies like noninterference and observational determinism, but has also found applications beyond security, e.g., distributed protocols and coding theory. However, HyperLTL satisfiability is undecidable as soon as there are existential quantifiers in the scope of a universal one. To overcome this severe limitation to applicability, we investigate here restricted variants of the satisfiability problem to pinpoint the decidability border.
First, we restrict the space of admissible models and show decidability when restricting the search space to models of bounded size or to finitely representable ones. Second, we consider formulas with restricted nesting of temporal operators and show that nesting depth one yields decidability for a slightly larger class of quantifier prefixes. We provide tight complexity bounds in almost all cases.
Cite as
Corto Mascle and Martin Zimmermann. The Keys to Decidable HyperLTL Satisfiability: Small Models or Very Simple Formulas. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 29:1-29:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{mascle_et_al:LIPIcs.CSL.2020.29,
author = {Mascle, Corto and Zimmermann, Martin},
title = {{The Keys to Decidable HyperLTL Satisfiability: Small Models or Very Simple Formulas}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {29:1--29:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.29},
URN = {urn:nbn:de:0030-drops-116720},
doi = {10.4230/LIPIcs.CSL.2020.29},
annote = {Keywords: Hyperproperties, Linear Temporal Logic, Satisfiability}
}
Document
Revisiting the Duality of Computation: An Algebraic Analysis of Classical Realizability Models
Abstract
In an impressive series of papers, Krivine showed at the edge of the last decade how classical realizability provides a surprising technique to build models for classical theories. In particular, he proved that classical realizability subsumes Cohen’s forcing, and even more, gives rise to unexpected models of set theories. Pursuing the algebraic analysis of these models that was first undertaken by Streicher, Miquel recently proposed to lay the algebraic foundation of classical realizability and forcing within new structures which he called implicative algebras. These structures are a generalization of Boolean algebras based on an internal law representing the implication. Notably, implicative algebras allow for the adequate interpretation of both programs (i.e. proofs) and their types (i.e. formulas) in the same structure.
The very definition of implicative algebras takes position on a presentation of logic through universal quantification and the implication and, computationally, relies on the call-by-name λ-calculus. In this paper, we investigate the relevance of this choice, by introducing two similar structures. On the one hand, we define disjunctive algebras, which rely on internal laws for the negation and the disjunction and which we show to be particular cases of implicative algebras. On the other hand, we introduce conjunctive algebras, which rather put the focus on conjunctions and on the call-by-value evaluation strategy. We finally show how disjunctive and conjunctive algebras algebraically reflect the well-known duality of computation between call-by-name and call-by-value.
Cite as
Étienne Miquey. Revisiting the Duality of Computation: An Algebraic Analysis of Classical Realizability Models. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 30:1-30:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{miquey:LIPIcs.CSL.2020.30,
author = {Miquey, \'{E}tienne},
title = {{Revisiting the Duality of Computation: An Algebraic Analysis of Classical Realizability Models}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {30:1--30:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.30},
URN = {urn:nbn:de:0030-drops-116734},
doi = {10.4230/LIPIcs.CSL.2020.30},
annote = {Keywords: realizability, model theory, forcing, proofs-as-programs, \lambda-calculus, classical logic, duality, call-by-value, call-by-name, lattices, tripos}
}
Document
Separation and Renaming in Nominal Sets
Abstract
Nominal sets provide a foundation for reasoning about names. They are used primarily in syntax with binders, but also, e.g., to model automata over infinite alphabets. In this paper, nominal sets are related to nominal renaming sets, which involve arbitrary substitutions rather than permutations, through a categorical adjunction. In particular, the left adjoint relates the separated product of nominal sets to the Cartesian product of nominal renaming sets. Based on these results, we define the new notion of separated nominal automata. We show that these automata can be exponentially smaller than classical nominal automata, if the semantics is closed under substitutions.
Cite as
Joshua Moerman and Jurriaan Rot. Separation and Renaming in Nominal Sets. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 31:1-31:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{moerman_et_al:LIPIcs.CSL.2020.31,
author = {Moerman, Joshua and Rot, Jurriaan},
title = {{Separation and Renaming in Nominal Sets}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {31:1--31:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.31},
URN = {urn:nbn:de:0030-drops-116744},
doi = {10.4230/LIPIcs.CSL.2020.31},
annote = {Keywords: Nominal sets, Separated product, Adjunction, Automata, Coalgebra}
}
Document
Parity Games: Another View on Lehtinen’s Algorithm
Abstract
Recently, five quasi-polynomial-time algorithms solving parity games were proposed. We elaborate on one of the algorithms, by Lehtinen (2018).
Czerwiński et al. (2019) observe that four of the algorithms can be expressed as constructions of separating automata (of quasi-polynomial size), that is, automata that accept all plays decisively won by one of the players, and rejecting all plays decisively won by the other player. The separating automata corresponding to three of the algorithms are deterministic, and it is clear that deterministic separating automata can be used to solve parity games. The separating automaton corresponding to the algorithm of Lehtinen is nondeterministic, though. While this particular automaton can be used to solve parity games, this is not true for every nondeterministic separating automaton. As a first (more conceptual) contribution, we specify when a nondeterministic separating automaton can be used to solve parity games.
We also repeat the correctness proof of the Lehtinen’s algorithm, using separating automata. In this part, we prove that her construction actually leads to a faster algorithm than originally claimed in her paper: its complexity is n^{O(log n)} rather than n^{O(log d ⋅ log n)} (where n is the number of nodes, and d the number of priorities of a considered parity game), which is similar to complexities of the other quasi-polynomial-time algorithms.
Cite as
Paweł Parys. Parity Games: Another View on Lehtinen’s Algorithm. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 32:1-32:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{parys:LIPIcs.CSL.2020.32,
author = {Parys, Pawe{\l}},
title = {{Parity Games: Another View on Lehtinen’s Algorithm}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {32:1--32:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.32},
URN = {urn:nbn:de:0030-drops-116757},
doi = {10.4230/LIPIcs.CSL.2020.32},
annote = {Keywords: Parity games, quasi-polynomial time, separating automata, good-for-games automata}
}
Document
De Jongh’s Theorem for Intuitionistic Zermelo-Fraenkel Set Theory
Abstract
We prove that the propositional logic of intuitionistic set theory IZF is intuitionistic propositional logic IPC. More generally, we show that IZF has the de Jongh property with respect to every intermediate logic that is complete with respect to a class of finite trees. The same results follow for constructive set theory CZF.
Cite as
Robert Passmann. De Jongh’s Theorem for Intuitionistic Zermelo-Fraenkel Set Theory. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 33:1-33:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{passmann:LIPIcs.CSL.2020.33,
author = {Passmann, Robert},
title = {{De Jongh’s Theorem for Intuitionistic Zermelo-Fraenkel Set Theory}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {33:1--33:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.33},
URN = {urn:nbn:de:0030-drops-116767},
doi = {10.4230/LIPIcs.CSL.2020.33},
annote = {Keywords: Intuitionistic Logic, Intuitionistic Set Theory, Constructive Set Theory}
}
Document
Computing Haar Measures
Abstract
According to Haar’s Theorem, every compact topological group G admits a unique (regular, right and) left-invariant Borel probability measure μ_G. Let the Haar integral (of G) denote the functional ∫_G:?(G)∋ f ↦ ∫ f d μ_G integrating any continuous function f:G → ℝ with respect to μ_G. This generalizes, and recovers for the additive group G=[0;1)mod 1, the usual Riemann integral: computable (cmp. Weihrauch 2000, Theorem 6.4.1), and of computational cost characterizing complexity class #P_1 (cmp. Ko 1991, Theorem 5.32).
We establish that in fact, every computably compact computable metric group renders the Haar measure/integral computable: once using an elegant synthetic argument, exploiting uniqueness in a computably compact space of probability measures; and once presenting and analyzing an explicit, imperative algorithm based on "maximum packings" with rigorous error bounds and guaranteed convergence. Regarding computational complexity, for the groups SO(3) and SU(2), we reduce the Haar integral to and from Euclidean/Riemann integration. In particular both also characterize #P_1.
Cite as
Arno Pauly, Dongseong Seon, and Martin Ziegler. Computing Haar Measures. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 34:1-34:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{pauly_et_al:LIPIcs.CSL.2020.34,
author = {Pauly, Arno and Seon, Dongseong and Ziegler, Martin},
title = {{Computing Haar Measures}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {34:1--34:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.34},
URN = {urn:nbn:de:0030-drops-116779},
doi = {10.4230/LIPIcs.CSL.2020.34},
annote = {Keywords: Computable analysis, topological groups, exact real arithmetic, Haar measure}
}
Document
The Call-By-Value Lambda-Calculus with Generalized Applications
Abstract
The lambda-calculus with generalized applications is the Curry-Howard counterpart to the system of natural deduction with generalized elimination rules for intuitionistic implicational logic. In this paper we identify a call-by-value variant of the system and prove confluence, strong normalization, and standardization. In the end, we show that the cbn and cbv variants of the system simulate each other via mappings based on extensions of the "protecting-by-a-lambda" compilation technique.
Cite as
José Espírito Santo. The Call-By-Value Lambda-Calculus with Generalized Applications. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 35:1-35:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{espiritosanto:LIPIcs.CSL.2020.35,
author = {Esp{\'\i}rito Santo, Jos\'{e}},
title = {{The Call-By-Value Lambda-Calculus with Generalized Applications}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {35:1--35:12},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.35},
URN = {urn:nbn:de:0030-drops-116786},
doi = {10.4230/LIPIcs.CSL.2020.35},
annote = {Keywords: Generalized applications, Natural deduction, Strong normalization, Standardization, Call-by-name, Call-by-value, Protecting-by-a-lambda}
}
Document
Dynamic Complexity Meets Parameterised Algorithms
Abstract
Dynamic Complexity studies the maintainability of queries with logical formulas in a setting where the underlying structure or database changes over time. Most often, these formulas are from first-order logic, giving rise to the dynamic complexity class DynFO. This paper investigates extensions of DynFO in the spirit of parameterised algorithms. In this setting structures come with a parameter k and the extensions allow additional "space" of size f(k) (in the form of an additional structure of this size) or additional time f(k) (in the form of iterations of formulas) or both. The resulting classes are compared with their non-dynamic counterparts and other classes. The main part of the paper explores the applicability of methods for parameterised algorithms to this setting through case studies for various well-known parameterised problems.
Cite as
Jonas Schmidt, Thomas Schwentick, Nils Vortmeier, Thomas Zeume, and Ioannis Kokkinis. Dynamic Complexity Meets Parameterised Algorithms. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 36:1-36:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{schmidt_et_al:LIPIcs.CSL.2020.36,
author = {Schmidt, Jonas and Schwentick, Thomas and Vortmeier, Nils and Zeume, Thomas and Kokkinis, Ioannis},
title = {{Dynamic Complexity Meets Parameterised Algorithms}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {36:1--36:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.36},
URN = {urn:nbn:de:0030-drops-116792},
doi = {10.4230/LIPIcs.CSL.2020.36},
annote = {Keywords: Dynamic complexity, parameterised complexity}
}
Document
Dynamic Complexity of Parity Exists Queries
Abstract
Given a graph whose nodes may be coloured red, the parity of the number of red nodes can easily be maintained with first-order update rules in the dynamic complexity framework DynFO of Patnaik and Immerman. Can this be generalised to other or even all queries that are definable in first-order logic extended by parity quantifiers? We consider the query that asks whether the number of nodes that have an edge to a red node is odd. Already this simple query of quantifier structure parity-exists is a major roadblock for dynamically capturing extensions of first-order logic.
We show that this query cannot be maintained with quantifier-free first-order update rules, and that variants induce a hierarchy for such update rules with respect to the arity of the maintained auxiliary relations. Towards maintaining the query with full first-order update rules, it is shown that degree-restricted variants can be maintained.
Cite as
Nils Vortmeier and Thomas Zeume. Dynamic Complexity of Parity Exists Queries. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 37:1-37:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{vortmeier_et_al:LIPIcs.CSL.2020.37,
author = {Vortmeier, Nils and Zeume, Thomas},
title = {{Dynamic Complexity of Parity Exists Queries}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {37:1--37:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.37},
URN = {urn:nbn:de:0030-drops-116805},
doi = {10.4230/LIPIcs.CSL.2020.37},
annote = {Keywords: Dynamic complexity, parity quantifier, arity hierarchy}
}