35 Search Results for "Frank, Yves"

Document
DOI: 10.4230/LIPIcs.FORC.2026.20
Privacy, Prediction, and Allocation

Authors: Ben Jacobsen and Nitin Kohli

Published in: LIPIcs, Volume 368, 7th Symposium on Foundations of Responsible Computing (FORC 2026)

Abstract
Algorithmic predictions are increasingly used to inform the allocation of scarce resources. The promise of these methods is that, through machine learning, they can better identify the people who would benefit most from interventions. Recently, however, several works have called this assumption into question by demonstrating the existence of settings where simple, unit-level allocation strategies can meet or even exceed the performance of those based on individual-level targeting. Separately, other works have objected to individual-level targeting on privacy grounds, leading to an unusual situation where a single solution, unit-level targeting, is recommended for reasons of both privacy and utility. Motivated by the desire to fully understand the interplay of privacy and targeting levels, we initiate the study of aid allocation systems that satisfy differential privacy, synthesizing existing works on private optimization with the economic models of aid allocation used in the non-private literature. To this end, we investigate private variants of both individual and unit-level allocation strategies in both stochastic and distribution-free settings under a range of constraints on data availability. Through this analysis, we provide clean, interpretable bounds characterizing the tradeoffs between privacy, efficiency, and targeting precision in allocation.
Cite as

Ben Jacobsen and Nitin Kohli. Privacy, Prediction, and Allocation. In 7th Symposium on Foundations of Responsible Computing (FORC 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 368, pp. 20:1-20:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{jacobsen_et_al:LIPIcs.FORC.2026.20,
  author =	{Jacobsen, Ben and Kohli, Nitin},
  title =	{{Privacy, Prediction, and Allocation}},
  booktitle =	{7th Symposium on Foundations of Responsible Computing (FORC 2026)},
  pages =	{20:1--20:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-419-2},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{368},
  editor =	{Lin, Huijia (Rachel)},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FORC.2026.20},
  URN =		{urn:nbn:de:0030-drops-259935},
  doi =		{10.4230/LIPIcs.FORC.2026.20},
  annote =	{Keywords: Differential privacy, fair allocation, limits of prediction}
}
Document
DOI: 10.4230/LIPIcs.SoCG.2026.79
D-GRIL: End-To-End Topological Learning with 2-Parameter Persistence

Authors: Soham Mukherjee, Shreyas N. Samaga, Cheng Xin, Steve Oudot, and Tamal K. Dey

Published in: LIPIcs, Volume 367, 42nd International Symposium on Computational Geometry (SoCG 2026)

Abstract
End-to-end topological learning using 1-parameter persistence is well-known. We show that the framework can be enhanced using 2-parameter persistence by adopting a recently introduced 2-parameter persistence based vectorization technique called Gril. We establish a theory for gradient descent on Gril producing D-Gril. We show that D-Gril can be used to learn a bifiltration function on benchmark graph datasets. Further, we exhibit that this framework can be applied in the context of bio-activity prediction in drug discovery.
Cite as

Soham Mukherjee, Shreyas N. Samaga, Cheng Xin, Steve Oudot, and Tamal K. Dey. D-GRIL: End-To-End Topological Learning with 2-Parameter Persistence. In 42nd International Symposium on Computational Geometry (SoCG 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 367, pp. 79:1-79:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{mukherjee_et_al:LIPIcs.SoCG.2026.79,
  author =	{Mukherjee, Soham and Samaga, Shreyas N. and Xin, Cheng and Oudot, Steve and Dey, Tamal K.},
  title =	{{D-GRIL: End-To-End Topological Learning with 2-Parameter Persistence}},
  booktitle =	{42nd International Symposium on Computational Geometry (SoCG 2026)},
  pages =	{79:1--79:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-418-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{367},
  editor =	{Ahn, Hee-Kap and Hoffmann, Michael and Nayyeri, Amir},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SoCG.2026.79},
  URN =		{urn:nbn:de:0030-drops-258865},
  doi =		{10.4230/LIPIcs.SoCG.2026.79},
  annote =	{Keywords: Topological Data Analysis, Persistent Homology, Multiparameter Persistence, Graph Learning, Graph Neural Networks}
}
Document
Survey
DOI: 10.4230/TGDK.4.1.2
Temporal Modelling in Cultural Heritage Knowledge Graphs: Use Cases, Requirements, Evaluation, and Decision Support

Authors: Oleksandra Bruns, Jörg Waitelonis, Jeff Z. Pan, and Harald Sack

Published in: TGDK, Volume 4, Issue 1 (2026). Transactions on Graph Data and Knowledge, Volume 4, Issue 1

Abstract
Our culture, history and world are in constant motion, continuously shaped by the flow of time, evolving narratives, and shifting relationships. Capturing this temporal complexity within cultural heritage (CH) knowledge graphs is essential for preserving the dynamic nature of human heritage. However, standard RDF predicates fail to effectively model the temporal aspects of cultural data, such as changing facts, evolving relationships, and temporal concepts. Over the past two decades, a variety of RDF-based approaches have been proposed to address this limitation, yet guidance is missing on which method best suits specific CH contexts. This paper presents a systematic evaluation of temporal RDF modelling approaches from a CH perspective. Based on an analysis of real-world CH use cases, core temporal requirements are identified that reflect both modelling expressivity and practical concerns. Six prominent approaches - RDF*, tRDF, Named Graphs, Singleton Property, N-ary Relations, and 4D Fluents - are assessed across these requirements. Our findings reveal that no single solution fits all scenarios, but suitable approaches can be selected based on project-specific priorities. To support practitioners, a decision-support tool is introduced to guide them in selecting the most suitable extension for their specific needs. This work provides practical guidance for CH modelling and contributes to the broader development of temporally aware Linked Data.
Cite as

Oleksandra Bruns, Jörg Waitelonis, Jeff Z. Pan, and Harald Sack. Temporal Modelling in Cultural Heritage Knowledge Graphs: Use Cases, Requirements, Evaluation, and Decision Support. In Transactions on Graph Data and Knowledge (TGDK), Volume 4, Issue 1, pp. 2:1-2:46, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@Article{bruns_et_al:TGDK.4.1.2,
  author =	{Bruns, Oleksandra and Waitelonis, J\"{o}rg and Pan, Jeff Z. and Sack, Harald},
  title =	{{Temporal Modelling in Cultural Heritage Knowledge Graphs: Use Cases, Requirements, Evaluation, and Decision Support}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{2:1--2:46},
  ISSN =	{2942-7517},
  year =	{2026},
  volume =	{4},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.4.1.2},
  URN =		{urn:nbn:de:0030-drops-256871},
  doi =		{10.4230/TGDK.4.1.2},
  annote =	{Keywords: Temporal Data Representation, RDF Extensions, Cultural Heritage, Knowledge Graphs}
}
Document
Research
DOI: 10.4230/TGDK.4.1.3
Semantically Reflected Programs

Authors: Eduard Kamburjan, Vidar Norstein Klungre, Yuanwei Qu, Rudolf Schlatte, Egor V. Kostylev, Martin Giese, and Einar Broch Johnsen

Published in: TGDK, Volume 4, Issue 1 (2026). Transactions on Graph Data and Knowledge, Volume 4, Issue 1

Abstract
This paper addresses the dichotomy between the formalization of structural and the formalization of executable behavioral knowledge by means of semantically lifted programs, which explore an intuitive connection between imperative programs and knowledge graphs. While knowledge graphs and ontologies are eminently useful to represent formal knowledge about a system’s individuals and universals, programming languages are designed to describe the system’s evolution. To address this dichotomy, we introduce a semantic lifting of the program states of an executing progam into a knowledge graph, for an object-oriented programming language. The resulting graph is exposed as a semantic reflection layer within the programming language, allowing programmers to leverage knowledge of the application domain in their programs during execution. In this paper, we formalize semantic lifting and semantic reflection for a small imperative programming language, SMOL, explain the operational aspects of the language, and consider type correctness and virtualization for runtime program queries through the semantic reflection layer. We illustrate semantic lifting and semantic reflection through a case study of geological modeling and discuss different applications of the technique. The language implementation is open source and available online.
Cite as

Eduard Kamburjan, Vidar Norstein Klungre, Yuanwei Qu, Rudolf Schlatte, Egor V. Kostylev, Martin Giese, and Einar Broch Johnsen. Semantically Reflected Programs. In Transactions on Graph Data and Knowledge (TGDK), Volume 4, Issue 1, pp. 3:1-3:52, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@Article{kamburjan_et_al:TGDK.4.1.3,
  author =	{Kamburjan, Eduard and Klungre, Vidar Norstein and Qu, Yuanwei and Schlatte, Rudolf and Kostylev, Egor V. and Giese, Martin and Johnsen, Einar Broch},
  title =	{{Semantically Reflected Programs}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{3:1--3:52},
  ISSN =	{2942-7517},
  year =	{2026},
  volume =	{4},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.4.1.3},
  URN =		{urn:nbn:de:0030-drops-256884},
  doi =		{10.4230/TGDK.4.1.3},
  annote =	{Keywords: Knowledge Graphs, Ontologies, Object-Oriented Modelling, Imperative Programming Languages, Reflection, Type Safety}
}
Document
DOI: 10.4230/OASIcs.NINeS.2026.24
SwiftQueue: Optimizing Low-Latency Applications with Swift Packet Queuing

Authors: Siddhant Ray, Xi Jiang, Jack Luo, Nick Feamster, and Junchen Jiang

Published in: OASIcs, Volume 139, 1st New Ideas in Networked Systems (NINeS 2026)

Abstract
Low Latency, Low Loss, and Scalable Throughput (L4S), as an emerging router-queue management technique, has seen steady deployment in the industry. An L4S-enabled router assigns each packet to the queue based on the packet header marking. Currently, L4S employs per-flow queue selection, i.e., all packets of a flow are marked the same way and thus use the same queues, even though each packet is marked separately. However, this may hurt tail latency and latency-sensitive applications because transient congestion and queue buildups may only affect a fraction of packets in a flow. We present SwiftQueue, a new L4S queue-selection strategy in which a sender uses a novel per-packet latency predictor to pinpoint which packets likely have latency spikes or drops. The insight is that many packet-level latency variations result from complex interactions among recent packets at shared router queues. Yet, these intricate packet-level latency patterns are hard to learn efficiently by traditional models. Instead, SwiftQueue uses a custom Transformer, which is well-studied for its expressiveness on sequential patterns, to predict the next packet’s latency based on the latencies of recently received ACKs. Based on the predicted latency of each outgoing packet, SwiftQueue’s sender dynamically marks the L4S packet header to assign packets to potentially different queues, even within the same flow. Using real network traces, we show that SwiftQueue is 45-65% more accurate in predicting latency and its variations than state-of-art methods. Based on its latency prediction, SwiftQueue reduces the tail latency for L4S-enabled flows by 36-45%, compared with the existing L4S queue-selection method.
Cite as

Siddhant Ray, Xi Jiang, Jack Luo, Nick Feamster, and Junchen Jiang. SwiftQueue: Optimizing Low-Latency Applications with Swift Packet Queuing. In 1st New Ideas in Networked Systems (NINeS 2026). Open Access Series in Informatics (OASIcs), Volume 139, pp. 24:1-24:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{ray_et_al:OASIcs.NINeS.2026.24,
  author =	{Ray, Siddhant and Jiang, Xi and Luo, Jack and Feamster, Nick and Jiang, Junchen},
  title =	{{SwiftQueue: Optimizing Low-Latency Applications with Swift Packet Queuing}},
  booktitle =	{1st New Ideas in Networked Systems (NINeS 2026)},
  pages =	{24:1--24:29},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-414-7},
  ISSN =	{2190-6807},
  year =	{2026},
  volume =	{139},
  editor =	{Argyraki, Katerina and Panda, Aurojit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.NINeS.2026.24},
  URN =		{urn:nbn:de:0030-drops-256093},
  doi =		{10.4230/OASIcs.NINeS.2026.24},
  annote =	{Keywords: Latency prediction, L4S Queue Management}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2026.104
Dimension-Free Correlated Sampling for the Hypersimplex

Authors: Joseph (Seffi) Naor, Nitya Raju, Abhishek Shetty, Aravind Srinivasan, Renata Valieva, and David Wajc

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

Abstract
Sampling from multiple distributions so as to maximize overlap has been studied by statisticians since the 1950s. Since the 2000s, such correlated sampling from the probability simplex has been a powerful building block in disparate areas of theoretical computer science. We study a generalization of this problem to sampling sets from given vectors in the hypersimplex, i.e., outputting sets of size (at most) k ∈ [n], while maximizing the overlap of the sampled sets. Specifically, the expected difference between two output sets should be at most α times their input vectors' 𝓁₁ distance. A value of α = O(log n) is known to be achievable, due to Chen et al. (ICALP'17). We improve this factor to O(log k), independent of the ambient dimension n. Our algorithm satisfies other desirable properties, including (up to a log^* n factor) input-sparsity sampling time, logarithmic parallel depth and dynamic update time, as well as preservation of submodular objectives. Anticipating broader use of correlated sampling algorithms for the hypersimplex, we present applications of our algorithm to online paging, offline approximation of metric multi-labeling, and swift multi-scenario submodular welfare approximating reallocation.
Cite as

Joseph (Seffi) Naor, Nitya Raju, Abhishek Shetty, Aravind Srinivasan, Renata Valieva, and David Wajc. Dimension-Free Correlated Sampling for the Hypersimplex. In 17th Innovations in Theoretical Computer Science Conference (ITCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 362, pp. 104:1-104:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{naor_et_al:LIPIcs.ITCS.2026.104,
  author =	{Naor, Joseph (Seffi) and Raju, Nitya and Shetty, Abhishek and Srinivasan, Aravind and Valieva, Renata and Wajc, David},
  title =	{{Dimension-Free Correlated Sampling for the Hypersimplex}},
  booktitle =	{17th Innovations in Theoretical Computer Science Conference (ITCS 2026)},
  pages =	{104:1--104:20},
  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.104},
  URN =		{urn:nbn:de:0030-drops-253918},
  doi =		{10.4230/LIPIcs.ITCS.2026.104},
  annote =	{Keywords: Correlated Rounding, Dependent Rounding}
}
Document
DOI: 10.4230/LIPIcs.IPEC.2025.21
A Polynomial Delay Algorithm Generating All Potential Maximal Cliques in Triconnected Planar Graphs

Authors: Alexander Grigoriev, Yasuaki Kobayashi, Hisao Tamaki, and Tom C. van der Zanden

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

Abstract
We develop a new characterization of potential maximal cliques of a triconnected planar graph and, using this characterization, give a polynomial delay algorithm generating all potential maximal cliques of a given triconnected planar graph. Combined with the dynamic programming algorithm due to Bouchitté and Todinca, this algorithm leads to a treewidth algorithm for general planar graphs that runs in time linear in the number of potential maximal cliques and polynomial in the number of vertices.
Cite as

Alexander Grigoriev, Yasuaki Kobayashi, Hisao Tamaki, and Tom C. van der Zanden. A Polynomial Delay Algorithm Generating All Potential Maximal Cliques in Triconnected Planar Graphs. In 20th International Symposium on Parameterized and Exact Computation (IPEC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 358, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{grigoriev_et_al:LIPIcs.IPEC.2025.21,
  author =	{Grigoriev, Alexander and Kobayashi, Yasuaki and Tamaki, Hisao and van der Zanden, Tom C.},
  title =	{{A Polynomial Delay Algorithm Generating All Potential Maximal Cliques in Triconnected Planar Graphs}},
  booktitle =	{20th International Symposium on Parameterized and Exact Computation (IPEC 2025)},
  pages =	{21:1--21:17},
  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.21},
  URN =		{urn:nbn:de:0030-drops-251530},
  doi =		{10.4230/LIPIcs.IPEC.2025.21},
  annote =	{Keywords: potential maximal cliques, treewidth, planar graphs, triconnected planar graphs, polynomial delay generation}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2025.5
Distributed Games with a Central Decision Maker

Authors: Bharat Adsul and Nehul Jain

Published in: LIPIcs, Volume 360, 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)

Abstract
We study distributed games played on non-deterministic asynchronous automata which feature a central decision maker process that participates in all key decision making tasks. In these partial-information games, processes use their causal past to respond to scheduling choices made by the scheduler and cooperatively strategize as a team to achieve the winning objective. We show that the problem of deciding the existence of a distributed winning strategy is efficiently solvable for global safety and local parity objectives. We provide algorithmic solutions that match their computational hardness. We formulate the notion of a finite-state distributed strategy which allows to quantify its distributed memory requirements. For the aforementioned objectives, we establish that finite-state distributed winning strategies always exist. In fact, we provide novel constructions of such winning strategies which are shown to have almost optimal amount of distributed memory. We also show that a natural extension of the model with two decision making processes is undecidable.
Cite as

Bharat Adsul and Nehul Jain. Distributed Games with a Central Decision Maker. In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 5:1-5:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{adsul_et_al:LIPIcs.FSTTCS.2025.5,
  author =	{Adsul, Bharat and Jain, Nehul},
  title =	{{Distributed Games with a Central Decision Maker}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{5:1--5:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-406-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{360},
  editor =	{Aiswarya, C. and Mehta, Ruta and Roy, Subhajit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.5},
  URN =		{urn:nbn:de:0030-drops-250843},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.5},
  annote =	{Keywords: Mazurkiewicz traces, models of concurrency, distributed synthesis, game-theoretic models, asynchronous automata, distributed decision-making}
}
Document
DOI: 10.4230/LIPIcs.DISC.2025.26
Towards Constant Time Multi-Call Rumor Spreading on Small-Set Expanders

Authors: Emilio Cruciani, Sebastian Forster, and Tijn de Vos

Published in: LIPIcs, Volume 356, 39th International Symposium on Distributed Computing (DISC 2025)

Abstract
We study a multi-call variant of the classic PUSH&PULL rumor spreading process where nodes can contact k of their neighbors instead of a single one during both PUSH and PULL operations. We show that rumor spreading can be made faster at the cost of an increased amount of communication between the nodes. As a motivating example, consider the process on a complete graph of n nodes: while the standard PUSH&PULL protocol takes Θ(log n) rounds, we prove that our k-PUSH&PULL variant completes in Θ(log_{k} n) rounds, with high probability. We generalize this result in an expansion-sensitive way, as has been done for the classic PUSH&PULL protocol for different notions of expansion, e.g., conductance and vertex expansion. We consider small-set vertex expanders, graphs in which every sufficiently small subset of nodes has a large neighborhood, ensuring strong local connectivity. In particular, when the expansion parameter satisfies ϕ > 1, these graphs have a diameter of o(log n), as opposed to other standard notions of expansion. Since the graph’s diameter is a lower bound on the number of rounds required for rumor spreading, this makes small-set expanders particularly well-suited for fast information dissemination. We prove that k-PUSH&PULL takes O(log_{ϕ} n ⋅ log_{k} n) rounds in these expanders, with high probability. We complement this with a simple lower bound of Ω(log_{ϕ} n+ log_{k} n) rounds.
Cite as

Emilio Cruciani, Sebastian Forster, and Tijn de Vos. Towards Constant Time Multi-Call Rumor Spreading on Small-Set Expanders. In 39th International Symposium on Distributed Computing (DISC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 356, pp. 26:1-26:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{cruciani_et_al:LIPIcs.DISC.2025.26,
  author =	{Cruciani, Emilio and Forster, Sebastian and de Vos, Tijn},
  title =	{{Towards Constant Time Multi-Call Rumor Spreading on Small-Set Expanders}},
  booktitle =	{39th International Symposium on Distributed Computing (DISC 2025)},
  pages =	{26:1--26:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-402-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{356},
  editor =	{Kowalski, Dariusz R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2025.26},
  URN =		{urn:nbn:de:0030-drops-248434},
  doi =		{10.4230/LIPIcs.DISC.2025.26},
  annote =	{Keywords: small set expansion, vertex expansion, rumor spreading, multi-call rumor spreading, push\&pull protocol}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.5
A Mechanized First-Order Theory of Algebraic Data Types with Pattern Matching

Authors: Joshua M. Cohen

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

Abstract
Algebraic data types (ADTs) and pattern matching are widely used to write elegant functional programs and to specify program behavior. These constructs are critical to most general-purpose interactive theorem provers (e.g. Lean, Rocq/Coq), first-order SMT-based deductive verifiers (e.g. Dafny, VeriFast), and intermediate verification languages (e.g. Why3). Such features require layers of compilation - in Rocq, pattern matches are compiled to remove nesting, while SMT-based tools further axiomatize ADTs with a first-order specification. However, these critical steps have been omitted from prior formalizations of such toolchains (e.g. MetaRocq). We give the first proved-sound sophisticated pattern matching compiler (based on Maranget’s compilation to decision trees) and first-order axiomatization of ADTs, both based on Why3 implementations. We prove the soundness of exhaustiveness checking, extending pen-and-paper proofs from the literature, and formulate a robustness property with which we find an exhaustiveness-related bug in Why3. We show that many of our proofs could be useful for reasoning about any first-order program verifier supporting ADTs.
Cite as

Joshua M. Cohen. A Mechanized First-Order Theory of Algebraic Data Types with Pattern Matching. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 5:1-5:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{cohen:LIPIcs.ITP.2025.5,
  author =	{Cohen, Joshua M.},
  title =	{{A Mechanized First-Order Theory of Algebraic Data Types with Pattern Matching}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{5:1--5:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.5},
  URN =		{urn:nbn:de:0030-drops-246046},
  doi =		{10.4230/LIPIcs.ITP.2025.5},
  annote =	{Keywords: Pattern Matching Compilation, Algebraic Data Types, First-Order Logic}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.14
Canonical for Automated Theorem Proving in Lean

Authors: Chase Norman and Jeremy Avigad

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

Abstract
Canonical is a solver for type inhabitation in dependent type theory, that is, the problem of producing a term of a given type. We present a Lean tactic which invokes Canonical to generate proof terms and synthesize programs. The tactic supports higher-order and dependently-typed goals, structural recursion over indexed inductive types, and definitional equality. Canonical finds proofs for 84% of Natural Number Game problems in 51 seconds total.
Cite as

Chase Norman and Jeremy Avigad. Canonical for Automated Theorem Proving in Lean. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{norman_et_al:LIPIcs.ITP.2025.14,
  author =	{Norman, Chase and Avigad, Jeremy},
  title =	{{Canonical for Automated Theorem Proving in Lean}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{14:1--14:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.14},
  URN =		{urn:nbn:de:0030-drops-246128},
  doi =		{10.4230/LIPIcs.ITP.2025.14},
  annote =	{Keywords: Automated Reasoning, Interactive Theorem Proving, Dependent Type Theory, Inhabitation, Unification, Program Synthesis, Formal Methods}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.26
Computational Complexity of Covering Regular Trees

Authors: Jan Bok, Jiří Fiala, Nikola Jedličková, and Jan Kratochvíl

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

Abstract
A graph covering projection, also referred to as a locally bijective homomorphism, is a mapping between the vertices and edges of two graphs that preserves incidences and is a local bijection. This concept originates in topological graph theory but has also found applications in combinatorics and theoretical computer science. In this paper we consider undirected graphs in the most general setting - graphs may contain multiple edges, loops, and semi-edges. This is in line with recent trends in topological graph theory and mathematical physics. We advance the study of the computational complexity of the H-Cover problem, which asks whether an input graph allows a covering projection onto a parameter graph H. The quest for a complete characterization started in 1990’s. Several results for simple graphs or graphs without semi-edges have been known, the role of semi-edges in the complexity setting has started to be investigated only recently. One of the most general known NP-hardness results states that H-Cover is NP-complete for every simple connected regular graph of valency greater than two. We complement this result by considering regular graphs H arising from connected acyclic graphs by adding semi-edges. Namely, we prove that any graph obtained by adding semi-edges to the vertices of a tree making it a d-regular graph with d ≥ 3, defines an NP-complete graph covering problem. In line with the so called Strong Dichotomy Conjecture, we prove that the NP-hardness holds even for simple graphs on input.
Cite as

Jan Bok, Jiří Fiala, Nikola Jedličková, and Jan Kratochvíl. Computational Complexity of Covering Regular Trees. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 26:1-26:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bok_et_al:LIPIcs.MFCS.2025.26,
  author =	{Bok, Jan and Fiala, Ji\v{r}{\'\i} and Jedli\v{c}kov\'{a}, Nikola and Kratochv{\'\i}l, Jan},
  title =	{{Computational Complexity of Covering Regular Trees}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{26:1--26:19},
  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.26},
  URN =		{urn:nbn:de:0030-drops-241338},
  doi =		{10.4230/LIPIcs.MFCS.2025.26},
  annote =	{Keywords: graph cover, covering projection, semi-edges, multigraphs, complexity, constrained homomorphisms, trees}
}
Document
DOI: 10.4230/LIPIcs.GIScience.2025.12
Large Multi-Modal Model Cartographic Map Comprehension for Textual Locality Georeferencing

Authors: Kalana Wijegunarathna, Kristin Stock, and Christopher B. Jones

Published in: LIPIcs, Volume 346, 13th International Conference on Geographic Information Science (GIScience 2025)

Abstract
Millions of biological sample records collected in the last few centuries archived in natural history collections are un-georeferenced. Georeferencing complex locality descriptions associated with these collection samples is a highly labour-intensive task collection agencies struggle with. None of the existing automated methods exploit maps that are an essential tool for georeferencing complex relations. We present preliminary experiments and results of a novel method that exploits multi-modal capabilities of recent Large Multi-Modal Models (LMM). This method enables the model to visually contextualize spatial relations it reads in the locality description. We use a grid-based approach to adapt these auto-regressive models for this task in a zero-shot setting. Our experiments conducted on a small manually annotated dataset show impressive results for our approach (∼1 km Average distance error) compared to uni-modal georeferencing with Large Language Models and existing georeferencing tools. The paper also discusses the findings of the experiments in light of an LMM’s ability to comprehend fine-grained maps. Motivated by these results, a practical framework is proposed to integrate this method into a georeferencing workflow.
Cite as

Kalana Wijegunarathna, Kristin Stock, and Christopher B. Jones. Large Multi-Modal Model Cartographic Map Comprehension for Textual Locality Georeferencing. In 13th International Conference on Geographic Information Science (GIScience 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 346, pp. 12:1-12:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{wijegunarathna_et_al:LIPIcs.GIScience.2025.12,
  author =	{Wijegunarathna, Kalana and Stock, Kristin and Jones, Christopher B.},
  title =	{{Large Multi-Modal Model Cartographic Map Comprehension for Textual Locality Georeferencing}},
  booktitle =	{13th International Conference on Geographic Information Science (GIScience 2025)},
  pages =	{12:1--12:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-378-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{346},
  editor =	{Sila-Nowicka, Katarzyna and Moore, Antoni and O'Sullivan, David and Adams, Benjamin and Gahegan, Mark},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.GIScience.2025.12},
  URN =		{urn:nbn:de:0030-drops-238412},
  doi =		{10.4230/LIPIcs.GIScience.2025.12},
  annote =	{Keywords: Large Multi-Modal Models, Large Language Models, LLM, Georeferencing, Natural History collections}
}
Document
DOI: 10.4230/LIPIcs.ECRTS.2025.18
Per-Flow Performance Guarantees in Networked Systems with Complex Feedback Structures

Authors: Anja Hamscher, Lukas Wildberger, and Jens Schmitt

Published in: LIPIcs, Volume 335, 37th Euromicro Conference on Real-Time Systems (ECRTS 2025)

Abstract
Many modern networked real-time systems encompass complex feedback structures and require stringent timing guarantees, especially bounds on the network delay. Network Calculus (NC) is a versatile methodology to compute such performance guarantees per individual flow; in particular, some fundamental results on how to deal with feedback exist. Yet, these are restricted to simple feedback structures and are mostly constrained to an analysis at the aggregate level (not per flow). In our work, we analyze more complex feedback structures than previously investigated by reducing them to canonical structures. We transform these closed-loop systems (with feedback) into open-loop systems (without feedback) and, subsequently, perform a per-flow analysis exploiting very recent NC results on per-flow performance guarantees. In a numerical experiment, we compare our new method to the current state-of-the-art which only allows for an aggregate FIFO analysis. We also compute how feedback constraints need to be allocated to ensure that a feedback system provides the same service as the system without feedback, in a sense providing for an optimal control. Furthermore, we compare different allocation strategies under a fixed budget for the feedback constraints.
Cite as

Anja Hamscher, Lukas Wildberger, and Jens Schmitt. Per-Flow Performance Guarantees in Networked Systems with Complex Feedback Structures. In 37th Euromicro Conference on Real-Time Systems (ECRTS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 335, pp. 18:1-18:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{hamscher_et_al:LIPIcs.ECRTS.2025.18,
  author =	{Hamscher, Anja and Wildberger, Lukas and Schmitt, Jens},
  title =	{{Per-Flow Performance Guarantees in Networked Systems with Complex Feedback Structures}},
  booktitle =	{37th Euromicro Conference on Real-Time Systems (ECRTS 2025)},
  pages =	{18:1--18:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-377-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{335},
  editor =	{Mancuso, Renato},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECRTS.2025.18},
  URN =		{urn:nbn:de:0030-drops-235961},
  doi =		{10.4230/LIPIcs.ECRTS.2025.18},
  annote =	{Keywords: Real-Time Networks, Network Calculus, Feedback Control}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.4
Substructural Parametricity

Authors: C. B. Aberlé, Karl Crary, Chris Martens, and Frank Pfenning

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

Abstract
Ordered, linear, and other substructural type systems allow us to expose deep properties of programs at the syntactic level of types. In this paper, we develop a family of unary logical relations that allow us to prove consequences of parametricity for a range of substructural type systems. A key idea is to parameterize the relation by an algebra, which we exemplify with a monoid and commutative monoid to interpret ordered and linear type systems, respectively. We prove the fundamental theorem of logical relations and apply it to deduce extensional properties of inhabitants of certain types. Examples include demonstrating that the ordered types for list append and reversal are inhabited by exactly one function, as are types of some tree traversals. Similarly, the linear type of the identity function on lists is inhabited only by permutations of the input. Our most advanced example shows that the ordered type of the list fold function is inhabited only by the fold function.
Cite as

C. B. Aberlé, Karl Crary, Chris Martens, and Frank Pfenning. Substructural Parametricity. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 4:1-4:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{aberle_et_al:LIPIcs.FSCD.2025.4,
  author =	{Aberl\'{e}, C. B. and Crary, Karl and Martens, Chris and Pfenning, Frank},
  title =	{{Substructural Parametricity}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{4:1--4:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.4},
  URN =		{urn:nbn:de:0030-drops-236193},
  doi =		{10.4230/LIPIcs.FSCD.2025.4},
  annote =	{Keywords: Substructural type systems, logical relations, ordered logic}
}
  • Refine by Type
  • 35 Document/PDF
  • 25 Document/HTML

  • Refine by Publication Year
  • 6 2026
  • 16 2025
  • 3 2024
  • 3 2023
  • 1 2022
  • Show More...

  • Refine by Author
  • 2 Calbimonte, Jean-Paul
  • 2 Giese, Martin
  • 2 Kamburjan, Eduard
  • 2 Rieg, Lionel
  • 2 Tamma, Valentina
  • Show More...

  • Refine by Series/Journal
  • 19 LIPIcs
  • 3 OASIcs
  • 5 LITES
  • 8 TGDK

  • Refine by Classification
  • 5 Computing methodologies → Knowledge representation and reasoning
  • 4 Computing methodologies → Ontology engineering
  • 3 Computer systems organization → Real-time systems
  • 3 Information systems → Semantic web description languages
  • 2 Mathematics of computing → Probabilistic algorithms
  • Show More...

  • Refine by Keyword
  • 3 Knowledge Graphs
  • 2 Knowledge graphs
  • 2 linear logic
  • 1 Abstract Interpretation
  • 1 Algebraic Data Types
  • 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