72 Search Results for "Durand, Arnaud"

Volume

LIPIcs, Volume 16

Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL

CSL 2012, September 3-6, 2012, Fontainebleau, France

Editors: Patrick Cégielski and Arnaud Durand

Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2026.162
Recursion and Proof Theoretical Characterizations of Small Circuit Classes with Modulo Counting via Discrete Differential Equations

Authors: Melissa Antonelli, Arnaud Durand, and Rui Li

Published in: LIPIcs, Volume 374, 53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026)

Abstract
The paper proposes an implicit (i.e., machine-independent) complexity approach to studying computation by polynomial-size, constant-depth circuits with gates counting modulo a constant through the lens of discrete ordinary differential equations (ODEs). So far, recursion-theoretic characterizations have been provided for functions computed by circuits of constant depth, including gates counting modulo 2 and 6 only (i.e., for the classes FAC⁰[2] and FAC⁰[6], resp.). In this paper, it is shown that considering ODE schemas, rather than bounded recursion, allows for a more fine-grained analysis, leading to (uniform) characterizations for all classes FAC⁰[n] (n ∈ ℕ), i.e. functions computed by circuits including counting modulo n gates. Inspired by the syntactic form of the ODE schemas, we go further in this direction and present first-order bounded theories for capturing provably total functions in each of these classes.
Cite as

Melissa Antonelli, Arnaud Durand, and Rui Li. Recursion and Proof Theoretical Characterizations of Small Circuit Classes with Modulo Counting via Discrete Differential Equations. In 53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 374, pp. 162:1-162:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{antonelli_et_al:LIPIcs.ICALP.2026.162,
  author =	{Antonelli, Melissa and Durand, Arnaud and Li, Rui},
  title =	{{Recursion and Proof Theoretical Characterizations of Small Circuit Classes with Modulo Counting via Discrete Differential Equations}},
  booktitle =	{53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026)},
  pages =	{162:1--162:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-428-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{374},
  editor =	{Bhattacharya, Sayan and Nanongkai, Danupon and Benedikt, Michael and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2026.162},
  URN =		{urn:nbn:de:0030-drops-265501},
  doi =		{10.4230/LIPIcs.ICALP.2026.162},
  annote =	{Keywords: Implicit complexity, circuit complexity, small circuit classes with counting, discrete ODEs, recursion theory, bounded arithmetic}
}
Document
DOI: 10.4230/LIPIcs.FUN.2026.16
Lozenge Tiling by Computing Distances

Authors: Jean-Marie Favreau, Yan Gerard, Pascal Lafourcade, and Léo Robert

Published in: LIPIcs, Volume 366, 13th International Conference on Fun with Algorithms (FUN 2026)

Abstract
The Calisson puzzle is a recent tiling game in which one must tile a triangular grid inside a hexagon with lozenges, under the constraint that certain prescribed edges must remain tile boundaries and that adjacent lozenges along these edges have different orientations. We present the first polynomial-time algorithm for this problem, with running time O(n³) for a hexagon of side length n. This algorithm, called the advancing surface algorithm, can be executed in a simple and intuitive way, even by hand with a pencil and an eraser. Its apparent simplicity conceals a deeper algorithmic reinterpretation of the classical ideas of John Conway and William Thurston, which we revisit from a theoretical computer science perspective. We introduce a graph-theoretic and difference constraints overlay that complements Thurston’s theory of lozenge tilings, revealing its intrinsic algorithmic structure and extending its scope to tiling problems with interior constraints and without necessarily boundary conditions. In Thurston’s approach, lozenge tilings are lifted to monotone stepped surfaces in the three-dimensional cubic lattice and projected back to the plane using height functions, reducing the tiling problem to the computation of heights. We show that, at an algorithmic level, selecting a monotone surface corresponds to selecting a directed cut (dicut) in a periodic directed graph, while height functions are solutions of a system of difference constraints. In this formulation, a region is tilable if and only if the associated weighted directed graph contains no cycle of strictly negative total weight. This new graph layer completing Thurston’s theory shows that Bellman–Ford’s shortest path algorithm is the only algorithmic primitive needed to decide feasibility and compute solutions. In particular, our framework allows us to decide whether the infinite triangular grid can be tiled while respecting a finite set of prescribed local constraints, a setting in which no boundary conditions are available.
Cite as

Jean-Marie Favreau, Yan Gerard, Pascal Lafourcade, and Léo Robert. Lozenge Tiling by Computing Distances. In 13th International Conference on Fun with Algorithms (FUN 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 366, pp. 16:1-16:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{favreau_et_al:LIPIcs.FUN.2026.16,
  author =	{Favreau, Jean-Marie and Gerard, Yan and Lafourcade, Pascal and Robert, L\'{e}o},
  title =	{{Lozenge Tiling by Computing Distances}},
  booktitle =	{13th International Conference on Fun with Algorithms (FUN 2026)},
  pages =	{16:1--16:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-417-8},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{366},
  editor =	{Iacono, John},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FUN.2026.16},
  URN =		{urn:nbn:de:0030-drops-257350},
  doi =		{10.4230/LIPIcs.FUN.2026.16},
  annote =	{Keywords: Tiling, Lozenge, Directed Graph, Dicut, Difference Constraints, Bellman-Ford}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.ICDT.2026.3
Building Relational Circuits (Invited Talk)

Authors: Florent Capelli

Published in: LIPIcs, Volume 365, 29th International Conference on Database Theory (ICDT 2026)

Abstract
We review two algorithms which allow to build a factorized representation of the answers set of join queries. In a nutshell, the representation builds a circuit representing the answers set of a join query by starting from atomic relations and iteratively combine them by either constructing the Cartesian product or the disjoint union of previously computed relations. The first one can be seen as the trace of the celebrated Yannakakis algorithm, building the answer set from the inputs to the output of the circuit while the second adopts a top-down approach which can be seen as a generalization of the exhaustive DPLL algorithm, originally designed to solve the #SAT problem.
Cite as

Florent Capelli. Building Relational Circuits (Invited Talk). In 29th International Conference on Database Theory (ICDT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 365, pp. 3:1-3:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{capelli:LIPIcs.ICDT.2026.3,
  author =	{Capelli, Florent},
  title =	{{Building Relational Circuits}},
  booktitle =	{29th International Conference on Database Theory (ICDT 2026)},
  pages =	{3:1--3:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-413-0},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{365},
  editor =	{ten Cate, Balder and Funk, Maurice},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2026.3},
  URN =		{urn:nbn:de:0030-drops-256172},
  doi =		{10.4230/LIPIcs.ICDT.2026.3},
  annote =	{Keywords: Conjunctive queries, factorized databases, knowledge compilation}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2026.9
Acyclic Join Sampling Under Selections: Dichotomy, Union Sampling, and Enumeration

Authors: Jinchao Huang, Yufei Tao, and Sibo Wang

Published in: LIPIcs, Volume 365, 29th International Conference on Database Theory (ICDT 2026)

Abstract
Previous research on join sampling has focused on joins without selection conditions, even though such conditions are prevalent in everyday queries in database systems. Motivated by this, we undertake a systematic investigation on the complexity of sampling from the result of an acyclic join under equality conditions given only at runtime. When conditions are conjunctive, the goal is to understand when it is possible to precompute a feasible structure that uses Õ(IN) space and supports sampling in Õ(1) time, where IN is the input size. We present a dichotomy to characterize (subject to a widely-accepted conjecture) the existence of such structures based on the conditions supplied and, in every feasible scenario, give an optimal structure of O(IN) space and O(1) sample time. We then extend our investigation to conditions expressed in disjunctive normal form, where the core challenge reduces to the fundamental set union sampling problem. We overcome the challenge with an optimal algorithm and utilize it to develop optimal sampling structures. Our findings also lead to new results on the closely-related random enumeration problem.
Cite as

Jinchao Huang, Yufei Tao, and Sibo Wang. Acyclic Join Sampling Under Selections: Dichotomy, Union Sampling, and Enumeration. In 29th International Conference on Database Theory (ICDT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 365, pp. 9:1-9:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{huang_et_al:LIPIcs.ICDT.2026.9,
  author =	{Huang, Jinchao and Tao, Yufei and Wang, Sibo},
  title =	{{Acyclic Join Sampling Under Selections: Dichotomy, Union Sampling, and Enumeration}},
  booktitle =	{29th International Conference on Database Theory (ICDT 2026)},
  pages =	{9:1--9:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-413-0},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{365},
  editor =	{ten Cate, Balder and Funk, Maurice},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2026.9},
  URN =		{urn:nbn:de:0030-drops-256231},
  doi =		{10.4230/LIPIcs.ICDT.2026.9},
  annote =	{Keywords: Conjunctive Queries, Acyclic Joins, Sampling, Lower Bounds}
}
Document
Database Theory in Action
DOI: 10.4230/LIPIcs.ICDT.2026.25
Database Theory in Action: Yannakakis' Algorithm

Authors: Paraschos Koutris, Stijn Vansummeren, Qichen Wang, Yisu Remy Wang, and Xiangyao Yu

Published in: LIPIcs, Volume 365, 29th International Conference on Database Theory (ICDT 2026)

Abstract
Yannakakis' seminal algorithm is optimal for acyclic joins, yet it has not been widely adopted due to its poor performance in practice. This paper briefly surveys recent advancements in making Yannakakis' algorithm more practical, in terms of both efficiency and ease of implementation, and points out several avenues for future research.
Cite as

Paraschos Koutris, Stijn Vansummeren, Qichen Wang, Yisu Remy Wang, and Xiangyao Yu. Database Theory in Action: Yannakakis' Algorithm. In 29th International Conference on Database Theory (ICDT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 365, pp. 25:1-25:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{koutris_et_al:LIPIcs.ICDT.2026.25,
  author =	{Koutris, Paraschos and Vansummeren, Stijn and Wang, Qichen and Wang, Yisu Remy and Yu, Xiangyao},
  title =	{{Database Theory in Action: Yannakakis' Algorithm}},
  booktitle =	{29th International Conference on Database Theory (ICDT 2026)},
  pages =	{25:1--25:6},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-413-0},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{365},
  editor =	{ten Cate, Balder and Funk, Maurice},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2026.25},
  URN =		{urn:nbn:de:0030-drops-256395},
  doi =		{10.4230/LIPIcs.ICDT.2026.25},
  annote =	{Keywords: Join algorithms, acyclicity, Yannakakis' algorithm}
}
Document
Database Theory in Action
DOI: 10.4230/LIPIcs.ICDT.2026.27
Database Theory in Action: Direct Access to Query Answers

Authors: Jiayin Hu and Nikolaos Tziavelis

Published in: LIPIcs, Volume 365, 29th International Conference on Database Theory (ICDT 2026)

Abstract
Direct access asks for the retrieval of query answers by their ranked position, given a query and a desired order. While the time complexity of data structures supporting such accesses has been studied in depth, and efficient algorithms for many queries and common orders are known, their practical performance has received little attention. We provide an implementation covering a wide range of queries and orders; it allows us to investigate intriguing practical aspects, including the comparative performance of database systems and the relationship between direct access and its single-access counterpart.
Cite as

Jiayin Hu and Nikolaos Tziavelis. Database Theory in Action: Direct Access to Query Answers. In 29th International Conference on Database Theory (ICDT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 365, pp. 27:1-27:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{hu_et_al:LIPIcs.ICDT.2026.27,
  author =	{Hu, Jiayin and Tziavelis, Nikolaos},
  title =	{{Database Theory in Action: Direct Access to Query Answers}},
  booktitle =	{29th International Conference on Database Theory (ICDT 2026)},
  pages =	{27:1--27:5},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-413-0},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{365},
  editor =	{ten Cate, Balder and Funk, Maurice},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2026.27},
  URN =		{urn:nbn:de:0030-drops-256411},
  doi =		{10.4230/LIPIcs.ICDT.2026.27},
  annote =	{Keywords: direct access, conjunctive queries, joins, ranking}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.47
Useful Call-by-Value: A Semantic Interpretation via Quantitative Types

Authors: Pablo Barenbaum, Delia Kesner, and Mariana Milicich

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

Abstract
Useful evaluation is an optimised evaluation mechanism for functional programming languages. It relies on representing terms with sharing and imposing a restricted notion of useful substitutions, that intuitively disallows copying subterms that do not contribute to the progress of the computation. In particular, useful call-by-value evaluation optimises the standard call-by-value strategy by preserving its original semantics. This preservation result has been shown by means of syntactical rewriting techniques, difficult to adapt to alternative variants of the calculi at play. In this work, we present the first semantic model of useful call-by-value evaluation through the non-idempotent intersection type system 𝒰. Our first contribution is a characterisation of termination for useful call-by-value evaluation via system 𝒰. That is, a term is typable in system 𝒰 if and only if it terminates in the useful call-by-value strategy. As a second contribution, we show that system 𝒰 provides a quantitative interpretation for useful call-by-value evaluation, offering exact step-count information for program evaluation. Our third contribution is that termination in call-by-value and useful call-by-value are equivalent. This ensures in particular that call-by-value, which is (potentially) erasing, and useful call-by-value, which is non-erasing, are observationally equivalent. Even though the specification of the operational semantics of useful evaluation is highly complex, system 𝒰 is notably simple. As far as we know, system 𝒰 is one of the scarce quantitative type systems capturing exactly the substitution step-count for variables and abstractions in an open call-by-value strategy.
Cite as

Pablo Barenbaum, Delia Kesner, and Mariana Milicich. Useful Call-by-Value: A Semantic Interpretation via Quantitative Types. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 47:1-47:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{barenbaum_et_al:LIPIcs.CSL.2026.47,
  author =	{Barenbaum, Pablo and Kesner, Delia and Milicich, Mariana},
  title =	{{Useful Call-by-Value: A Semantic Interpretation via Quantitative Types}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{47:1--47:24},
  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.47},
  URN =		{urn:nbn:de:0030-drops-254721},
  doi =		{10.4230/LIPIcs.CSL.2026.47},
  annote =	{Keywords: Lambda calculus, Evaluation strategies, Call-by-Value, Useful Evaluation, Intersection types, Quantitative models}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2026.46
Symmetric Algebraic Circuits and Homomorphism Polynomials

Authors: Anuj Dawar, Benedikt Pago, and Tim Seppelt

Published in: LIPIcs, Volume 362, 17th Innovations in Theoretical Computer Science Conference (ITCS 2026)

Abstract
The central open question of algebraic complexity is whether VP ≠ VNP, which is saying that the permanent cannot be represented by families of polynomial-size algebraic circuits. For symmetric algebraic circuits, this has been confirmed by Dawar and Wilsenach (2020), who showed exponential lower bounds on the size of symmetric circuits for the permanent. In this work, we set out to develop a more general symmetric algebraic complexity theory. Our main result is that a family of symmetric polynomials admits small symmetric circuits if and only if they can be written as a linear combination of homomorphism counting polynomials of graphs of bounded treewidth. We also establish a relationship between the symmetric complexity of subgraph counting polynomials and the vertex cover number of the pattern graph. As a concrete example, we examine the symmetric complexity of immanant families (a generalisation of the determinant and permanent) and show that a known conditional dichotomy due to Curticapean (2021) holds unconditionally in the symmetric setting.
Cite as

Anuj Dawar, Benedikt Pago, and Tim Seppelt. Symmetric Algebraic Circuits and Homomorphism Polynomials. In 17th Innovations in Theoretical Computer Science Conference (ITCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 362, pp. 46:1-46:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{dawar_et_al:LIPIcs.ITCS.2026.46,
  author =	{Dawar, Anuj and Pago, Benedikt and Seppelt, Tim},
  title =	{{Symmetric Algebraic Circuits and Homomorphism Polynomials}},
  booktitle =	{17th Innovations in Theoretical Computer Science Conference (ITCS 2026)},
  pages =	{46:1--46:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-410-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{362},
  editor =	{Saraf, Shubhangi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2026.46},
  URN =		{urn:nbn:de:0030-drops-253330},
  doi =		{10.4230/LIPIcs.ITCS.2026.46},
  annote =	{Keywords: algebraic complexity, finite model theory, symmetric circuits, homomorphism counting, graph homomorphism, treewidth, counting width, first-order logic with counting quantifiers}
}
Document
DOI: 10.4230/LIPIcs.IPEC.2025.23
Enumeration Kernels for Vertex Cover and Feedback Vertex Set

Authors: Marin Bougeret, Guilherme C. M. Gomes, Vinicius F. dos Santos, and Ignasi Sau

Published in: LIPIcs, Volume 358, 20th International Symposium on Parameterized and Exact Computation (IPEC 2025)

Abstract
Enumerative kernelization is a recent and promising area sitting at the intersection of parameterized complexity and enumeration algorithms. Its study began with the paper of Creignou et al. [Theory Comput. Syst., 2017], and development in the area has started to accelerate with the work of Golovach et al. [J. Comput. Syst. Sci., 2022]. The latter introduced polynomial-delay enumeration kernels and applied them in the study of structural parameterizations of the Matching Cut problem and some variants. Few other results, mostly on Longest Path and some generalizations of Matching Cut, have also been developed. However, little success has been seen in enumeration versions of Vertex Cover and Feedback Vertex Set, some of the most studied problems in kernelization. In this paper, we address this shortcoming. Our first result is a polynomial-delay enumeration kernel with 2k vertices for Enum Vertex Cover, where we wish to list all solutions with at most k vertices. This is obtained by developing a non-trivial lifting algorithm for the classical crown decomposition reduction rule, and directly improves upon the kernel with 𝒪(k²) vertices derived from the work of Creignou et al. Our other result is a polynomial-delay enumeration kernel with 𝒪(k³) vertices and edges for Enum Feedback Vertex Set; the proof is inspired by some ideas of Thomassé [TALG, 2010], but with a weaker bound on the kernel size due to difficulties in applying the q-expansion technique.
Cite as

Marin Bougeret, Guilherme C. M. Gomes, Vinicius F. dos Santos, and Ignasi Sau. Enumeration Kernels for Vertex Cover and Feedback Vertex Set. In 20th International Symposium on Parameterized and Exact Computation (IPEC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 358, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bougeret_et_al:LIPIcs.IPEC.2025.23,
  author =	{Bougeret, Marin and C. M. Gomes, Guilherme and dos Santos, Vinicius F. and Sau, Ignasi},
  title =	{{Enumeration Kernels for Vertex Cover and Feedback Vertex Set}},
  booktitle =	{20th International Symposium on Parameterized and Exact Computation (IPEC 2025)},
  pages =	{23:1--23:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-407-9},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{358},
  editor =	{Agrawal, Akanksha and van Leeuwen, Erik Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.IPEC.2025.23},
  URN =		{urn:nbn:de:0030-drops-251552},
  doi =		{10.4230/LIPIcs.IPEC.2025.23},
  annote =	{Keywords: Kernelization, Enumeration, Vertex cover, Crown decomposition, Feedback vertex set}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.10
Characterizing Small Circuit Classes from FAC⁰ to FAC¹ via Discrete Ordinary Differential Equations

Authors: Melissa Antonelli, Arnaud Durand, and Juha Kontinen

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

Abstract
In this paper, we provide a uniform framework for investigating small circuit classes and bounds through the lens of ordinary differential equations (ODEs). Following an approach recently introduced to capture the class of polynomial-time computable functions via ODE-based recursion schemas and later applied to the context of functions computed by unbounded fan-in circuits of constant depth (FAC⁰), we study multiple relevant small circuit classes. In particular, we show that natural restrictions on linearity and derivation along functions with specific growth rate correspond to kinds of functions that can be proved to be in various classes, ranging from FAC⁰ to FAC¹. This reveals an intriguing link between constraints over linear-length ODEs and circuit computation, providing new tools to tackle the complex challenge of establishing bounds for classes in the circuit hierarchies and possibly enhancing our understanding of the role of counters in this setting. Additionally, we establish several completeness results, in particular obtaining the first ODE-based characterizations for the classes of functions computable in constant depth with unbounded fan-in and Mod 2 gates (FACC[2]) and in logarithmic depth with bounded fan-in Boolean gates (FNC¹).
Cite as

Melissa Antonelli, Arnaud Durand, and Juha Kontinen. Characterizing Small Circuit Classes from FAC⁰ to FAC¹ via Discrete Ordinary Differential Equations. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{antonelli_et_al:LIPIcs.MFCS.2025.10,
  author =	{Antonelli, Melissa and Durand, Arnaud and Kontinen, Juha},
  title =	{{Characterizing Small Circuit Classes from FAC⁰ to FAC¹ via Discrete Ordinary Differential Equations}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{10:1--10:18},
  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.10},
  URN =		{urn:nbn:de:0030-drops-241170},
  doi =		{10.4230/LIPIcs.MFCS.2025.10},
  annote =	{Keywords: Implicit computational complexity, parallel computation, function algebras, ordinary differential equations, circuit complexity}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.19
Monotone Bounded-Depth Complexity of Homomorphism Polynomials

Authors: C.S. Bhargav, Shiteng Chen, Radu Curticapean, and Prateek Dwivedi

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

Abstract
For every fixed graph H, it is known that homomorphism counts from H and colorful H-subgraph counts can be determined in O(n^{t+1}) time on n-vertex input graphs G, where t is the treewidth of H. On the other hand, a running time of n^{o(t / log t)} would refute the exponential-time hypothesis. Komarath, Pandey, and Rahul (Algorithmica, 2023) studied algebraic variants of these counting problems, i.e., homomorphism and subgraph polynomials for fixed graphs H. These polynomials are weighted sums over the objects counted above, where each object is weighted by the product of variables corresponding to edges contained in the object. As shown by Komarath et al., the monotone circuit complexity of the homomorphism polynomial for H is Θ(n^{tw(H)+1}). In this paper, we characterize the power of monotone bounded-depth circuits for homomorphism and colorful subgraph polynomials. This leads us to discover a natural hierarchy of graph parameters tw_Δ(H), for fixed Δ ∈ ℕ, which capture the width of tree-decompositions for H when the underlying tree is required to have depth at most Δ. We prove that monotone circuits of product-depth Δ computing the homomorphism polynomial for H require size Θ(n^{tw_Δ(H^{†})+1}), where H^{†} is the graph obtained from H by removing all degree-1 vertices. This allows us to derive an optimal depth hierarchy theorem for monotone bounded-depth circuits through graph-theoretic arguments.
Cite as

C.S. Bhargav, Shiteng Chen, Radu Curticapean, and Prateek Dwivedi. Monotone Bounded-Depth Complexity of Homomorphism Polynomials. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 19:1-19:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bhargav_et_al:LIPIcs.MFCS.2025.19,
  author =	{Bhargav, C.S. and Chen, Shiteng and Curticapean, Radu and Dwivedi, Prateek},
  title =	{{Monotone Bounded-Depth Complexity of Homomorphism Polynomials}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{19:1--19:18},
  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.19},
  URN =		{urn:nbn:de:0030-drops-241269},
  doi =		{10.4230/LIPIcs.MFCS.2025.19},
  annote =	{Keywords: algebraic complexity, homomorphisms, monotone circuit complexity, bounded-depth circuits, treewidth, pathwidth}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.69
FO-Query Enumeration over SLP-Compressed Structures of Bounded Degree

Authors: Markus Lohrey, Sebastian Maneth, and Markus L. Schmid

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

Abstract
Enumerating the result set of a first-order query over a relational structure of bounded degree can be done with linear preprocessing and constant delay. In this work, we extend this result towards the compressed perspective where the structure is given in a potentially highly compressed form by a straight-line program (SLP). Our main result is an algorithm that enumerates the result set of a first-order query over a structure of bounded degree that is represented by an SLP satisfying the so-called apex condition. For a fixed formula, the enumeration algorithm has constant delay and needs a preprocessing time that is linear in the size of the SLP.
Cite as

Markus Lohrey, Sebastian Maneth, and Markus L. Schmid. FO-Query Enumeration over SLP-Compressed Structures of Bounded Degree. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 69:1-69:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lohrey_et_al:LIPIcs.MFCS.2025.69,
  author =	{Lohrey, Markus and Maneth, Sebastian and Schmid, Markus L.},
  title =	{{FO-Query Enumeration over SLP-Compressed Structures of Bounded Degree}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{69:1--69:20},
  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.69},
  URN =		{urn:nbn:de:0030-drops-241760},
  doi =		{10.4230/LIPIcs.MFCS.2025.69},
  annote =	{Keywords: Enumeration algorithms, FO-logic, query evaluation over compressed data}
}
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.24
Fair Termination of Asynchronous Binary Sessions

Authors: Luca Padovani and Gianluigi Zavattaro

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

Abstract
We study a theory of asynchronous session types ensuring that well-typed processes terminate under a suitable fairness assumption. Fair termination entails starvation freedom and orphan message freedom namely that all messages, including those that are produced early taking advantage of asynchrony, are eventually consumed. The theory is based on a novel fair asynchronous subtyping relation for session types that is coarser than the existing ones. The type system is also the first of its kind that is firmly rooted in linear logic: fair asynchronous subtyping is incorporated as a natural generalization of the cut and axiom rules of linear logic and asynchronous communication is modeled through a suitable set of commuting conversions and of deep cut reductions in linear logic proofs.
Cite as

Luca Padovani and Gianluigi Zavattaro. Fair Termination of Asynchronous Binary Sessions. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 24:1-24:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{padovani_et_al:LIPIcs.ECOOP.2025.24,
  author =	{Padovani, Luca and Zavattaro, Gianluigi},
  title =	{{Fair Termination of Asynchronous Binary Sessions}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{24:1--24: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.24},
  URN =		{urn:nbn:de:0030-drops-233169},
  doi =		{10.4230/LIPIcs.ECOOP.2025.24},
  annote =	{Keywords: Binary sessions, fair asynchronous subtyping, fair termination, linear logic}
}
  • Refine by Type
  • 71 Document/PDF
  • 18 Document/HTML
  • 1 Volume

  • Refine by Publication Year
  • 8 2026
  • 11 2025
  • 1 2024
  • 1 2022
  • 1 2021
  • Show More...

  • Refine by Author
  • 13 Durand, Arnaud
  • 4 Kontinen, Juha
  • 3 Antonelli, Melissa
  • 3 Capelli, Florent
  • 3 Dawar, Anuj
  • Show More...

  • Refine by Series/Journal
  • 70 LIPIcs
  • 1 DagSemProc

  • Refine by Classification
  • 5 Theory of computation → Circuit complexity
  • 3 Theory of computation → Complexity classes
  • 3 Theory of computation → Database query processing and optimization (theory)
  • 3 Theory of computation → Database theory
  • 2 Information systems → Relational database model
  • Show More...

  • Refine by Keyword
  • 5 finite model theory
  • 4 algebraic complexity
  • 3 circuit complexity
  • 2 Classical Logic
  • 2 Conjunctive Queries
  • 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