39 Search Results for "Werner, Martin"

Document
DOI: 10.4230/LIPIcs.ITCS.2026.57
Anti-Concentration for the Unitary Haar Measure and Applications to Random Quantum Circuits

Authors: Bill Fefferman, Soumik Ghosh, and Wei Zhan

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

Abstract
We prove a Carbery-Wright style anti-concentration inequality for the unitary Haar measure, by showing that the probability of a polynomial in the entries of a random unitary falling into an ε range is at most a polynomial in ε. Using it, we show that the scrambling speed of a random quantum circuit is lower bounded: Namely, every input qubit has an influence that is at least inverse exponential in depth, on any output qubit touched by its lightcone. Our result on scrambling speed works with high probability over the choice of a circuit from an ensemble, as opposed to just working in expectation. As an application, we give the first polynomial-time algorithm for learning log-depth random quantum circuits with Haar random gates up to polynomially small diamond distance, given oracle access to the circuit. Other applications of this new scrambling speed lower bound include: - An optimal Ω(log ε^{-1}) depth lower bound for ε-approximate unitary designs on any circuit architecture; - A polynomial-time quantum algorithm that computes the depth of a bounded-depth circuit, given oracle access to the circuit. Our learning and depth-testing algorithms apply to architectures defined over any geometric dimension, and can be generalized to a wide class of architectures with good lightcone properties.
Cite as

Bill Fefferman, Soumik Ghosh, and Wei Zhan. Anti-Concentration for the Unitary Haar Measure and Applications to Random Quantum Circuits. In 17th Innovations in Theoretical Computer Science Conference (ITCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 362, pp. 57:1-57:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{fefferman_et_al:LIPIcs.ITCS.2026.57,
  author =	{Fefferman, Bill and Ghosh, Soumik and Zhan, Wei},
  title =	{{Anti-Concentration for the Unitary Haar Measure and Applications to Random Quantum Circuits}},
  booktitle =	{17th Innovations in Theoretical Computer Science Conference (ITCS 2026)},
  pages =	{57:1--57:24},
  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.57},
  URN =		{urn:nbn:de:0030-drops-253443},
  doi =		{10.4230/LIPIcs.ITCS.2026.57},
  annote =	{Keywords: Haar measure, anti-concentration, random quanytum circuit, learning}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2025.6
Foundations of Fiat-Denominated Loans Collateralized by Cryptocurrencies

Authors: Pavel Hubáček, Jan Václavek, and Michelle Yeo

Published in: LIPIcs, Volume 361, 29th International Conference on Principles of Distributed Systems (OPODIS 2025)

Abstract
The rising importance of cryptocurrencies as financial assets pushed their applicability from an object of speculation closer to standard financial instruments such as loans. In this work, we initiate the study of secure protocols that enable fiat-denominated loans collateralized by cryptocurrencies such as Bitcoin. We provide limited-custodial protocols for such loans relying only on trusted arbitration and provide their game-theoretical analysis. We also highlight various interesting directions for future research.
Cite as

Pavel Hubáček, Jan Václavek, and Michelle Yeo. Foundations of Fiat-Denominated Loans Collateralized by Cryptocurrencies. In 29th International Conference on Principles of Distributed Systems (OPODIS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 361, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{hubacek_et_al:LIPIcs.OPODIS.2025.6,
  author =	{Hub\'{a}\v{c}ek, Pavel and V\'{a}clavek, Jan and Yeo, Michelle},
  title =	{{Foundations of Fiat-Denominated Loans Collateralized by Cryptocurrencies}},
  booktitle =	{29th International Conference on Principles of Distributed Systems (OPODIS 2025)},
  pages =	{6:1--6:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-409-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{361},
  editor =	{Arusoaie, Andrei and Onica, Emanuel and Spear, Michael and Tucci-Piergiovanni, Sara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2025.6},
  URN =		{urn:nbn:de:0030-drops-251796},
  doi =		{10.4230/LIPIcs.OPODIS.2025.6},
  annote =	{Keywords: Blockchains, Cryptocurrencies, DeFi, Loans, Mechanism design, Subgame Perfect Equilibrium, Rational analysis}
}
Document
DOI: 10.4230/DagMan.11.1.1
Climate Change: What is Computing’s Responsibility? (Dagstuhl Perspectives Workshop 25122)

Authors: Bran Knowles, Vicki L. Hanson, Christoph Becker, Mike Berners-Lee, Andrew A. Chien, Benoit Combemale, Vlad Coroamă, Koen De Bosschere, Yi Ding, Adrian Friday, Boris Gamazaychikov, Lynda Hardman, Simon Hinterholzer, Mattias Höjer, Lynn Kaack, Lenneke Kuijer, Anne-Laure Ligozat, Jan Tobias Muehlberg, Yunmook Nah, Thomas Olsson, Anne-Cécile Orgerie, Daniel Pargman, Birgit Penzenstadler, Tom Romanoff, Emma Strubell, Colin Venters, and Junhua Zhao

Published in: Dagstuhl Manifestos, Volume 11, Issue 1 (2025)

Abstract
This Manifesto was produced from the Perspectives Workshop 25122 entitled "Climate Change: What is Computing’s Responsibility?" held March 16-19, 2025 at Schloss Dagstuhl, Germany. The Workshop provided a forum for world-leading computer scientists and expert consultants on environmental policy and sustainable transition to engage in a critical and urgent conversation about computing’s responsibilities in addressing climate change - or more aptly, climate crisis. The resulting Manifesto outlines commitments and directions for future action which, if adopted as a basis for more responsible computing practices, will help ensure that these technologies do not threaten the long-term habitability of the planet. We preface our Manifesto with a recognition that humanity is on a path that is not in agreement with international global warming targets and explore how computing technologies are currently hastening the overshoot of these boundaries. We critically assess the vaunted potential for harnessing computing technologies for the mitigation of global warming, agreeing that, under current circumstances, computing is contributing to negative environmental impacts in other sectors. Computing primarily improves efficiency and reduces costs which leads to more consumption and more negative environmental impact. Relying solely on efficiency gains in computing has thus far proven to be insufficient to curb global greenhouse gas emissions. Therefore, computing’s purpose within a strategy for tackling climate change must be reimagined. Our recommendations cover changes that need to be urgently made to the design priorities of computing technologies, but also speak to the more systemic shift in mindset, with sustainability and human rights providing a necessary moral foundation for developing the kinds of computing technologies most needed by society. We also stress the importance of digital policy that accounts for both the direct material impacts of computing and the detrimental indirect impacts arising from computing-enabled efficiencies, and the role of computing professionals in informing policy making.
Cite as

Bran Knowles, Vicki L. Hanson, Christoph Becker, Mike Berners-Lee, Andrew A. Chien, Benoit Combemale, Vlad Coroamă, Koen De Bosschere, Yi Ding, Adrian Friday, Boris Gamazaychikov, Lynda Hardman, Simon Hinterholzer, Mattias Höjer, Lynn Kaack, Lenneke Kuijer, Anne-Laure Ligozat, Jan Tobias Muehlberg, Yunmook Nah, Thomas Olsson, Anne-Cécile Orgerie, Daniel Pargman, Birgit Penzenstadler, Tom Romanoff, Emma Strubell, Colin Venters, and Junhua Zhao. Climate Change: What is Computing’s Responsibility? (Dagstuhl Perspectives Workshop 25122). In Dagstuhl Manifestos, Volume 11, Issue 1, pp. 1-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Article{knowles_et_al:DagMan.11.1.1,
  author =	{Knowles, Bran and Hanson, Vicki L. and Becker, Christoph and Berners-Lee, Mike and Chien, Andrew A. and Combemale, Benoit and Coroam\u{a}, Vlad and De Bosschere, Koen and Ding, Yi and Friday, Adrian and Gamazaychikov, Boris and Hardman, Lynda and Hinterholzer, Simon and H\"{o}jer, Mattias and Kaack, Lynn and Kuijer, Lenneke and Ligozat, Anne-Laure and Muehlberg, Jan Tobias and Nah, Yunmook and Olsson, Thomas and Orgerie, Anne-C\'{e}cile and Pargman, Daniel and Penzenstadler, Birgit and Romanoff, Tom and Strubell, Emma and Venters, Colin and Zhao, Junhua},
  title =	{{Climate Change: What is Computing’s Responsibility? (Dagstuhl Perspectives Workshop 25122)}},
  pages =	{1--18},
  journal =	{Dagstuhl Manifestos},
  ISSN =	{2193-2433},
  year =	{2025},
  volume =	{11},
  number =	{1},
  editor =	{Knowles, Bran and Hanson, Vicki L. and Becker, Christoph and Berners-Lee, Mike and Chien, Andrew A. and Combemale, Benoit and Coroam\u{a}, Vlad and De Bosschere, Koen and Ding, Yi and Friday, Adrian and Gamazaychikov, Boris and Hardman, Lynda and Hinterholzer, Simon and H\"{o}jer, Mattias and Kaack, Lynn and Kuijer, Lenneke and Ligozat, Anne-Laure and Muehlberg, Jan Tobias and Nah, Yunmook and Olsson, Thomas and Orgerie, Anne-C\'{e}cile and Pargman, Daniel and Penzenstadler, Birgit and Romanoff, Tom and Strubell, Emma and Venters, Colin and Zhao, Junhua},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagMan.11.1.1},
  URN =		{urn:nbn:de:0030-drops-250724},
  doi =		{10.4230/DagMan.11.1.1},
  annote =	{Keywords: sustainability, climate change, efficiency, supply chain management, climate modelling}
}
Document
DOI: 10.4230/LIPIcs.TIME.2025.5
Higher-Order Timed Automata and Tail Recursion

Authors: Florian Bruse

Published in: LIPIcs, Volume 355, 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)

Abstract
Timed Automata (TA) are a popular formalism to model systems in dense linear time. However, due to their finite state-space, they can only model systems with a finitary logical behavior. There are extensions to e.g., timed pushdown systems and timed recursive state machines. Higher-Order Recursion Schemes (HORS) are another popular model for infinite-state, non-regular systems, naturally stratified by their type-theoretic order. We recently introduced Real-Time Recursion schemes as an approximation of HORS to real-time systems. This paper updates Real-Time Recursion Schemes into Higher-Order Timed Automata, a formalism that defines a tree-shaped timed automaton, which is more suitable to model actual systems. We show that the model-checking problem against the timed version of the modal mu-calculus exhibits the expected complexity bounds, i.e., an increase by one exponential towards the untimed version. We also show that, in the presence of tail recursion, half an exponential can be recovered, mirroring similar gains in the untimed setting. We also give a matching lower bound for the special case of order-1 HORTA. We conjecture that this can be generalized for all orders.
Cite as

Florian Bruse. Higher-Order Timed Automata and Tail Recursion. In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 5:1-5:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bruse:LIPIcs.TIME.2025.5,
  author =	{Bruse, Florian},
  title =	{{Higher-Order Timed Automata and Tail Recursion}},
  booktitle =	{32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)},
  pages =	{5:1--5:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-401-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{355},
  editor =	{Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025.5},
  URN =		{urn:nbn:de:0030-drops-244519},
  doi =		{10.4230/LIPIcs.TIME.2025.5},
  annote =	{Keywords: Timed Automata, Higher-Order Recursion Schemes, Tree Automata, Tail Recursion}
}
Document
DOI: 10.4230/LIPIcs.ESA.2025.89
A Simple Algorithm for Trimmed Multipoint Evaluation

Authors: Nick Fischer, Melvin Kallmayer, and Leo Wennmann

Published in: LIPIcs, Volume 351, 33rd Annual European Symposium on Algorithms (ESA 2025)

Abstract
Evaluating a polynomial on a set of points is a fundamental task in computer algebra. In this work, we revisit a particular variant called trimmed multipoint evaluation: given an n-variate polynomial with bounded individual degree d and total degree D, the goal is to evaluate it on a natural class of input points. This problem arises as a key subroutine in recent algorithmic results [Dinur; SODA '21], [Dell, Haak, Kallmayer, Wennmann; SODA '25]. It is known that trimmed multipoint evaluation can be solved in near-linear time [van der Hoeven, Schost; AAECC '13] by a clever yet somewhat involved algorithm. We give a simple recursive algorithm that avoids heavy computer-algebraic machinery, and can be readily understood by researchers without specialized background.
Cite as

Nick Fischer, Melvin Kallmayer, and Leo Wennmann. A Simple Algorithm for Trimmed Multipoint Evaluation. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 89:1-89:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{fischer_et_al:LIPIcs.ESA.2025.89,
  author =	{Fischer, Nick and Kallmayer, Melvin and Wennmann, Leo},
  title =	{{A Simple Algorithm for Trimmed Multipoint Evaluation}},
  booktitle =	{33rd Annual European Symposium on Algorithms (ESA 2025)},
  pages =	{89:1--89:11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-395-9},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{351},
  editor =	{Benoit, Anne and Kaplan, Haim and Wild, Sebastian and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2025.89},
  URN =		{urn:nbn:de:0030-drops-245574},
  doi =		{10.4230/LIPIcs.ESA.2025.89},
  annote =	{Keywords: Algebraic Algorithms, Multipoint Evaluation, Interpolation, LU Decomposition}
}
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.CONCUR.2025.5
Characterizations of Fragments of Temporal Logic over Mazurkiewicz Traces

Authors: Bharat Adsul, Paul Gastin, and Shantanu Kulkarni

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
We study fragments of temporal logics over Mazurkiewicz traces which are well known and established partial-order models of concurrent behaviours. We focus on concurrent versions of "strict past" and "strict future" modalities. Over words, the corresponding fragments have been shown to coincide with natural algebraic conditions on the recognizing monoids. We provide non-trivial generalizations of these classical results to traces. We exploit the local nature of the temporal modalities and obtain modular translations of specifications into asynchronous automata. More specifically, we provide novel characterizations of these fragments via local cascade products of a very simple two-state asynchronous automaton operating on a single process.
Cite as

Bharat Adsul, Paul Gastin, and Shantanu Kulkarni. Characterizations of Fragments of Temporal Logic over Mazurkiewicz Traces. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 5:1-5:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{adsul_et_al:LIPIcs.CONCUR.2025.5,
  author =	{Adsul, Bharat and Gastin, Paul and Kulkarni, Shantanu},
  title =	{{Characterizations of Fragments of Temporal Logic over Mazurkiewicz Traces}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{5:1--5:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.5},
  URN =		{urn:nbn:de:0030-drops-239551},
  doi =		{10.4230/LIPIcs.CONCUR.2025.5},
  annote =	{Keywords: Mazurkiewicz traces, temporal logics, asynchronous automata, cascade product, Green’s relations, algebraic automata theory}
}
Document
DOI: 10.4230/LIPIcs.GIScience.2025.16
What, When, and Where Do You Mean? Detecting Spatio-Temporal Concept Drift in Scientific Texts

Authors: Meilin Shi, Krzysztof Janowicz, Zilong Liu, Mina Karimi, Ivan Majic, and Alexandra Fortacz

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

Abstract
Inundated by the rapidly expanding AI research nowadays, the research community requires more effective research data management than ever. A key challenge lies in the evolving nature of concepts embedded in the growing body of research publications. As concepts evolve over time (e.g., keywords like global warming become more commonly referred to as climate change), past research may become harder to find and interpret in a modern context. This phenomenon, known as concept drift, affects how research topics and keywords are understood, categorized, and retrieved. Beyond temporal drift, such variations also occur across geographic space, reflecting differences in local policies, research priorities, and so forth. In this work, we introduce the notion of spatio-temporal concept drift to capture how concepts in scientific texts evolve across both space and time. Using a scientometric dataset in geographic information science, we detect how research keywords drifted across countries and years using word embeddings. By detecting spatio-temporal concept drift, we can better align archival research and bridge regional differences, ensuring scientific knowledge remains findable and interoperable within evolving research landscapes.
Cite as

Meilin Shi, Krzysztof Janowicz, Zilong Liu, Mina Karimi, Ivan Majic, and Alexandra Fortacz. What, When, and Where Do You Mean? Detecting Spatio-Temporal Concept Drift in Scientific Texts. In 13th International Conference on Geographic Information Science (GIScience 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 346, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{shi_et_al:LIPIcs.GIScience.2025.16,
  author =	{Shi, Meilin and Janowicz, Krzysztof and Liu, Zilong and Karimi, Mina and Majic, Ivan and Fortacz, Alexandra},
  title =	{{What, When, and Where Do You Mean? Detecting Spatio-Temporal Concept Drift in Scientific Texts}},
  booktitle =	{13th International Conference on Geographic Information Science (GIScience 2025)},
  pages =	{16:1--16:18},
  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.16},
  URN =		{urn:nbn:de:0030-drops-238450},
  doi =		{10.4230/LIPIcs.GIScience.2025.16},
  annote =	{Keywords: Concept Drift, Ontology, Large Language Models, Research Data Management}
}
Document
DOI: 10.4230/OASIcs.SLATE.2025.3
Elements for Weighted Answer-Set Programming

Authors: Francisco Coelho, Bruno Dinis, Dietmar Seipel, and Salvador Abreu

Published in: OASIcs, Volume 135, 14th Symposium on Languages, Applications and Technologies (SLATE 2025)

Abstract
Logic programs, more specifically, answer-set programs, can be annotated with probabilities on facts to express uncertainty. We address the problem of propagating weight annotations on facts (e.g. probabilities) of an answer-set program to its stable models, and from there to events (defined as sets of atoms) in a dataset over the program’s domain. We propose a novel approach which is algebraic in the sense that it relies on an equivalence relation over the set of events. Uncertainty is then described as polynomial expressions over variables. We propagate the weight function in the space of models and events, rather than doing so within the syntax of the program. As evidence that our approach is sound, we show that certain facts behave as expected. Our approach allows us to investigate weight annotated programs and to determine how suitable a given one is for modeling a given dataset containing events. It’s core is illustrated by a running example and the encoding of a Bayesian network.
Cite as

Francisco Coelho, Bruno Dinis, Dietmar Seipel, and Salvador Abreu. Elements for Weighted Answer-Set Programming. In 14th Symposium on Languages, Applications and Technologies (SLATE 2025). Open Access Series in Informatics (OASIcs), Volume 135, pp. 3:1-3:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{coelho_et_al:OASIcs.SLATE.2025.3,
  author =	{Coelho, Francisco and Dinis, Bruno and Seipel, Dietmar and Abreu, Salvador},
  title =	{{Elements for Weighted Answer-Set Programming}},
  booktitle =	{14th Symposium on Languages, Applications and Technologies (SLATE 2025)},
  pages =	{3:1--3:16},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-387-4},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{135},
  editor =	{Baptista, Jorge and Barateiro, Jos\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SLATE.2025.3},
  URN =		{urn:nbn:de:0030-drops-236836},
  doi =		{10.4230/OASIcs.SLATE.2025.3},
  annote =	{Keywords: Answer-Set Programming, Stable Models, Probabilistic Logic Programming}
}
Document
DOI: 10.4230/LIPIcs.SEA.2025.4
U-Index: A Universal Indexing Framework for Matching Long Patterns

Authors: Lorraine A. K. Ayad, Gabriele Fici, Ragnar Groot Koerkamp, Grigorios Loukides, Rob Patro, Giulio Ermanno Pibiri, and Solon P. Pissis

Published in: LIPIcs, Volume 338, 23rd International Symposium on Experimental Algorithms (SEA 2025)

Abstract
Motivation. Text indexing is a fundamental and well-studied problem. Classic solutions to this problem either replace the original text with a compressed representation, e.g., the FM-index and its variants, or keep it uncompressed but attach some redundancy - an index - to accelerate matching, e.g., the suffix array. The former solutions thus retain excellent compressed space, but are practically slow to construct and query. The latter approaches, instead, sacrifice space efficiency but are typically faster; for example, the suffix array takes much more space than the text itself for commonly used alphabets, like ASCII or DNA, but it is very fast to construct and query. Methods. In this paper, we show that efficient text indexing can be achieved using just a small extra space on top of the original text, provided that the query patterns are sufficiently long. More specifically, we develop a new indexing paradigm in which a sketch of a query pattern is first matched against a sketch of the text. Once candidate matches are retrieved, they are verified using the original text. This paradigm is thus universal in the sense that it allows us to use any solution to index the sketched text, like a suffix array, FM-index, or r-index. Results. We explore both the theory and the practice of this universal framework. With an extensive experimental analysis, we show that, surprisingly, universal indexes can be constructed much faster than their unsketched counterparts and take a fraction of the space, as a direct consequence of (i) having a lower bound on the length of patterns and (ii) working in sketch space. Furthermore, these data structures have the potential of retaining or even improving query time, because matching against the sketched text is faster and verifying candidates can be theoretically done in constant time per occurrence (or, in practice, by short and cache-friendly scans of the text). Finally, we discuss some important applications of this novel indexing paradigm to computational biology. We hypothesize that such indexes will be particularly effective when the queries are sufficiently long, and so we demonstrate applications in long-read mapping.
Cite as

Lorraine A. K. Ayad, Gabriele Fici, Ragnar Groot Koerkamp, Grigorios Loukides, Rob Patro, Giulio Ermanno Pibiri, and Solon P. Pissis. U-Index: A Universal Indexing Framework for Matching Long Patterns. In 23rd International Symposium on Experimental Algorithms (SEA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 338, pp. 4:1-4:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ayad_et_al:LIPIcs.SEA.2025.4,
  author =	{Ayad, Lorraine A. K. and Fici, Gabriele and Groot Koerkamp, Ragnar and Loukides, Grigorios and Patro, Rob and Pibiri, Giulio Ermanno and Pissis, Solon P.},
  title =	{{U-Index: A Universal Indexing Framework for Matching Long Patterns}},
  booktitle =	{23rd International Symposium on Experimental Algorithms (SEA 2025)},
  pages =	{4:1--4:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-375-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{338},
  editor =	{Mutzel, Petra and Prezza, Nicola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SEA.2025.4},
  URN =		{urn:nbn:de:0030-drops-232420},
  doi =		{10.4230/LIPIcs.SEA.2025.4},
  annote =	{Keywords: Text Indexing, Sketching, Minimizers, Hashing}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.21
An Expressive Trace Logic for Recursive Programs

Authors: Dilian Gurov and Reiner Hähnle

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

Abstract
We present an expressive logic over trace formulas, based on binary state predicates, chop, and least fixed points, for precise specification of programs with recursive procedures. Both programs and trace formulas are equipped with a direct-style, fully compositional, denotational semantics that on programs coincides with the standard SOS of recursive programs. We design a compositional proof calculus for proving finite-trace program properties, and prove soundness as well as (relative) completeness. We show that each program can be mapped to a semantics-preserving trace formula and, vice versa, each trace formula can be mapped to a canonical program over slightly extended programs, resulting in a Galois connection between programs and formulas. Our results shed light on the correspondence between programming constructs and logical connectives.
Cite as

Dilian Gurov and Reiner Hähnle. An Expressive Trace Logic for Recursive Programs. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 21:1-21:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{gurov_et_al:LIPIcs.FSCD.2025.21,
  author =	{Gurov, Dilian and H\"{a}hnle, Reiner},
  title =	{{An Expressive Trace Logic for Recursive Programs}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{21:1--21:22},
  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.21},
  URN =		{urn:nbn:de:0030-drops-236360},
  doi =		{10.4230/LIPIcs.FSCD.2025.21},
  annote =	{Keywords: Denotational semantics, compositional semantics, program specification, compositional verification, fixed point logic, trace logic}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.6
Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems

Authors: Emma Ahrens, Jan-Christoph Kassing, Jürgen Giesl, and Joost-Pieter Katoen

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

Abstract
We present novel semiring semantics for abstract reduction systems (ARSs). More precisely, we provide a weighted version of ARSs, where the reduction steps induce weights from a semiring. Inspired by provenance analysis in database theory and logic, we obtain a formalism that can be used for provenance analysis of arbitrary ARSs. Our semantics handle (possibly unbounded) non-determinism and possibly infinite reductions. Moreover, we develop several techniques to prove upper and lower bounds on the weights resulting from our semantics, and show that in this way one obtains a uniform approach to analyze several different properties like termination, derivational complexity, space complexity, safety, as well as combinations of these properties.
Cite as

Emma Ahrens, Jan-Christoph Kassing, Jürgen Giesl, and Joost-Pieter Katoen. Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 6:1-6:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ahrens_et_al:LIPIcs.FSCD.2025.6,
  author =	{Ahrens, Emma and Kassing, Jan-Christoph and Giesl, J\"{u}rgen and Katoen, Joost-Pieter},
  title =	{{Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{6:1--6: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.6},
  URN =		{urn:nbn:de:0030-drops-236215},
  doi =		{10.4230/LIPIcs.FSCD.2025.6},
  annote =	{Keywords: Rewriting, Semirings, Semantics, Termination, Verification}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.31
Higher-Dimensional Automata: Extension to Infinite Tracks

Authors: Luc Passemard, Amazigh Amrane, and Uli Fahrenberg

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

Abstract
We introduce higher-dimensional automata for infinite interval ipomsets (ω-HDAs). We define key concepts from different points of view, inspired from their finite counterparts. Then we explore languages recognized by ω-HDAs under Büchi and Muller semantics. We show that Muller acceptance is more expressive than Büchi acceptance and, in contrast to the finite case, both semantics do not yield languages closed under subsumption. Then, we adapt the original rational operations to deal with ω-HDAs and show that while languages of ω-HDAs are ω-rational, not all ω-rational languages can be expressed by ω-HDAs.
Cite as

Luc Passemard, Amazigh Amrane, and Uli Fahrenberg. Higher-Dimensional Automata: Extension to Infinite Tracks. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 31:1-31:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{passemard_et_al:LIPIcs.FSCD.2025.31,
  author =	{Passemard, Luc and Amrane, Amazigh and Fahrenberg, Uli},
  title =	{{Higher-Dimensional Automata: Extension to Infinite Tracks}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{31:1--31:23},
  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.31},
  URN =		{urn:nbn:de:0030-drops-236466},
  doi =		{10.4230/LIPIcs.FSCD.2025.31},
  annote =	{Keywords: Higher-dimensional automata, concurrency theory, omega pomsets, B\"{u}chi acceptance, Muller acceptance, interval pomsets, pomsets with interfaces}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.27
What Does It Take to Certify a Conversion Checker?

Authors: Meven Lennon-Bertrand

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

Abstract
We report on a detailed exploration of the properties of conversion (definitional equality) in dependent type theory, with the goal of certifying decision procedures for it. While in that context the property of normalisation has attracted the most light, we instead emphasize the importance of injectivity properties, showing that they alone are both crucial and sufficient to certify most desirable properties of conversion checkers. We also explore the certification of a fully untyped conversion checker, with respect to a typed specification, and show that the story is mostly unchanged, although the exact injectivity properties needed are subtly different.
Cite as

Meven Lennon-Bertrand. What Does It Take to Certify a Conversion Checker?. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 27:1-27:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lennonbertrand:LIPIcs.FSCD.2025.27,
  author =	{Lennon-Bertrand, Meven},
  title =	{{What Does It Take to Certify a Conversion Checker?}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{27:1--27:23},
  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.27},
  URN =		{urn:nbn:de:0030-drops-236428},
  doi =		{10.4230/LIPIcs.FSCD.2025.27},
  annote =	{Keywords: Dependent types, Bidirectional typing, Certified software}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.4
Ensuring Convergence and Invariants Without Coordination

Authors: Dina Borrego, Nuno Preguiça, Elisa Gonzalez Boix, and Carla Ferreira

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

Abstract
The CAP theorem demonstrates a trade-off between consistency and availability (and, by extension, latency) in systems where network partitions are unavoidable, such as in cloud computing and local-first software. While adopting weak consistency can preserve availability, it may result in inconsistencies that compromise application correctness. Replicated data types provide a principled, coordination-free approach to guarantee convergence but do not consider application invariants. Existing methods for maintaining invariants in replicated systems either rely on coordination - undermining the benefits of weak consistency - or suffer from limited applicability. This paper introduces the No-Op framework, a generic approach for enforcing consistency without coordination while guaranteeing both convergence and invariant preservation. The core idea of the No-Op approach is to resolve conflicts among concurrent operations by prioritising one operation over the other according to programmer-defined conflict resolution policies. This prioritisation transforms the less-preferred operation into a no-side-effect operation, ensuring conflict-free execution. We formalise the model underlying the No-Op framework and introduce a replication protocol built upon it, accompanied by a formal proof of correctness for both the framework and the protocol. Furthermore, we demonstrate the framework’s applicability by showcasing the design of widely used replicated data types and the preservation of a wide range of application invariants.
Cite as

Dina Borrego, Nuno Preguiça, Elisa Gonzalez Boix, and Carla Ferreira. Ensuring Convergence and Invariants Without Coordination. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 4:1-4:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{borrego_et_al:LIPIcs.ECOOP.2025.4,
  author =	{Borrego, Dina and Pregui\c{c}a, Nuno and Gonzalez Boix, Elisa and Ferreira, Carla},
  title =	{{Ensuring Convergence and Invariants Without Coordination}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{4:1--4: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.4},
  URN =		{urn:nbn:de:0030-drops-232978},
  doi =		{10.4230/LIPIcs.ECOOP.2025.4},
  annote =	{Keywords: distributed systems, conflict resolution, RDTs, invariant preservation}
}
  • Refine by Type
  • 39 Document/PDF
  • 29 Document/HTML

  • Refine by Publication Year
  • 2 2026
  • 24 2025
  • 3 2024
  • 2 2023
  • 3 2022
  • Show More...

  • Refine by Author
  • 3 Werner, Christian
  • 3 Werner, Martin
  • 2 Hähnle, Reiner
  • 1 Abreu, Salvador
  • 1 Adsul, Bharat
  • Show More...

  • Refine by Series/Journal
  • 27 LIPIcs
  • 3 OASIcs
  • 4 LITES
  • 3 TGDK
  • 1 DagMan
  • Show More...

  • Refine by Classification
  • 4 Theory of computation → Logic and verification
  • 3 Theory of computation → Modal and temporal logics
  • 2 Information systems → Geographic information systems
  • 2 Theory of computation → Automata over infinite objects
  • 2 Theory of computation → Online algorithms
  • Show More...

  • Refine by Keyword
  • 2 OWL
  • 2 Scheduling
  • 2 Security
  • 1 3D city model
  • 1 Active Objects
  • 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