126 Search Results for "Lang, Martin"

Document
DOI: 10.4230/LIPIcs.SEA.2026.24
ZOR Filters: Fast and Smaller Than Fuse Filters

Authors: Antoine Limasset

Published in: LIPIcs, Volume 371, 24th International Symposium on Experimental Algorithms (SEA 2026)

Abstract
Probabilistic membership filters support fast approximate membership queries with controlled false-positive probability ε and are widely used across storage, analytics, networking, and bioinformatics [Chang et al., 2008; Niv Dayan et al., 2018; Broder and Mitzenmacher, 2004; Harris and Medvedev, 2020; Marchet and Limasset, 2023; Chikhi et al., 2025; Hernandez-Courbevoie et al., 2025]. In the static setting, low-overhead methods such as XOR, Fuse, and BuRR have been proposed [Graf and Lemire, 2020; Graf and Lemire, 2022; Dillinger et al., 2022; Ulrich and Renard, 2023]. Among these, Fuse filters are known for near-optimal query throughput. For XOR/Fuse-style peeling constructions, however, build success is only high probability, which complicates deterministic builds. We introduce ZOR filters, a deterministic continuation of XOR/Fuse-style constructions that guarantees termination while preserving the same XOR-based query mechanism. ZOR replaces restart-on-failure with deterministic peeling that abandons a small fraction of keys, and restores false-positive-only semantics by storing the remainder in a compact auxiliary structure. In our experiments, the abandoned fraction drops below 1% for moderate arity (e.g., N ≥ 5), so the auxiliary handles a negligible fraction of keys. As a result, ZOR filters can be substantially more memory-efficient than Fuse filters, with overhead below 1%, while not yet matching the near-optimal overhead of BuRR (below 0.1%). In query performance, ZOR-pure is close to Fuse and faster than BuRR on positive queries, while the complete interleaved variant trades additional negative-query latency for deterministic continuation. Relative to optimised Fuse/BuRR implementations [Graf and Lemire, 2022; Dillinger et al., 2022], the current ZOR prototype remains slower in construction because deterministic peeling requires explicit incidence handling; reducing this construction gap is an important direction for future work.
Cite as

Antoine Limasset. ZOR Filters: Fast and Smaller Than Fuse Filters. In 24th International Symposium on Experimental Algorithms (SEA 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 371, pp. 24:1-24:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{limasset:LIPIcs.SEA.2026.24,
  author =	{Limasset, Antoine},
  title =	{{ZOR Filters: Fast and Smaller Than Fuse Filters}},
  booktitle =	{24th International Symposium on Experimental Algorithms (SEA 2026)},
  pages =	{24:1--24:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-422-2},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{371},
  editor =	{Aum\"{u}ller, Martin and Finocchi, Irene},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SEA.2026.24},
  URN =		{urn:nbn:de:0030-drops-260281},
  doi =		{10.4230/LIPIcs.SEA.2026.24},
  annote =	{Keywords: Data structure, Approximate Set Membership, Static filter}
}
Document
DOI: 10.4230/LIPIcs.SEA.2026.18
DeltaSort: Incremental Sorting of Arrays with Known Updates

Authors: Shubham Dwivedi

Published in: LIPIcs, Volume 371, 24th International Symposium on Experimental Algorithms (SEA 2026)

Abstract
When records need to be read in a particular order, sorting at query time incurs repeated Θ(n log n) cost for an array of n records and can become a bottleneck in read-heavy workloads. A common solution is to maintain a derived sorted read-replica that is kept updated as the underlying system-of-record changes. For updating read-replicas that are stored as arrays, existing approaches rely on either full re-sorting or incremental algorithms such as binary insertion or merge-based sort. In this paper, we study incremental sorting under a new model in which the sorting routine is explicitly informed of the k indices updated since the previous sort - a setting that naturally arises in systems that track updates. Under this model, we present DeltaSort, a new algorithm that runs in O(n√k) expected time using O(k) auxiliary space under a random update model, and outperforms existing algorithms for small update batches in our experimental evaluation.
Cite as

Shubham Dwivedi. DeltaSort: Incremental Sorting of Arrays with Known Updates. In 24th International Symposium on Experimental Algorithms (SEA 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 371, pp. 18:1-18:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{dwivedi:LIPIcs.SEA.2026.18,
  author =	{Dwivedi, Shubham},
  title =	{{DeltaSort: Incremental Sorting of Arrays with Known Updates}},
  booktitle =	{24th International Symposium on Experimental Algorithms (SEA 2026)},
  pages =	{18:1--18:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-422-2},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{371},
  editor =	{Aum\"{u}ller, Martin and Finocchi, Irene},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SEA.2026.18},
  URN =		{urn:nbn:de:0030-drops-260224},
  doi =		{10.4230/LIPIcs.SEA.2026.18},
  annote =	{Keywords: Incremental sorting, Sorting algorithms, Array maintenance}
}
Document
DOI: 10.4230/LIPIcs.CPM.2026.10
R-Enum Revisited: Speedup and Extension for Context-Sensitive Repeats and Net Frequencies

Authors: Kotaro Kimura and Tomohiro I

Published in: LIPIcs, Volume 369, 37th Annual Symposium on Combinatorial Pattern Matching (CPM 2026)

Abstract
A repeat is a substring that occurs at least twice in a string, and is called a maximal repeat if it cannot be extended outwards without reducing its frequency. Nishimoto and Tabei [CPM, 2021] proposed r-enum, an algorithm to enumerate various characteristic substrings, including maximal repeats, in a string T of length n in O(r) words of compressed working space, where r ≤ n is the number of runs in the Burrows-Wheeler transform (BWT) of T. Given the run-length encoded BWT (RLBWT) of T, r-enum runs in O(n log log_w (n/r)) time in addition to the time linear to the number of output strings, where w = Θ(log n) is the word size. In this paper, we first improve the O(n log log_w (n/r)) term to O(n). We next extend r-enum to compute other context-sensitive repeats such as near-supermaximal repeats (NSMRs) and supermaximal repeats, as well as the context diversity for every maximal repeat in the same complexities. Furthermore, we study net occurrences: An occurrence of a repeat is called a net occurrence if it is not covered by another repeat, and the net frequency of a repeat is the number of its net occurrences. With this terminology, an NSMR is a repeat with a positive net frequency. Given the RLBWT of T, we show how to compute the set 𝒮^{nsmr} of all NSMRs in T together with their net frequency/occurrences in O(n) time and O(r) space. We also show that an O(r)-space data structure can be built from the RLBWT to compute the net frequency/occurrences of any pattern in optimal time. The data structure is built in O(r) space and in O(n) time with high probability or deterministic O(n + |𝒮^{nsmr}| log log min(σ, |𝒮^{nsmr}|)) time, where σ ≤ r is the alphabet size of T. To achieve this, we prove that the total number of net occurrences is less than 2r. With the duality between net occurrences and minimal unique substrings (MUSs), we get a new upper bound 2r of the number of MUSs in T, which may be of independent interest.
Cite as

Kotaro Kimura and Tomohiro I. R-Enum Revisited: Speedup and Extension for Context-Sensitive Repeats and Net Frequencies. In 37th Annual Symposium on Combinatorial Pattern Matching (CPM 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 369, pp. 10:1-10:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{kimura_et_al:LIPIcs.CPM.2026.10,
  author =	{Kimura, Kotaro and I, Tomohiro},
  title =	{{R-Enum Revisited: Speedup and Extension for Context-Sensitive Repeats and Net Frequencies}},
  booktitle =	{37th Annual Symposium on Combinatorial Pattern Matching (CPM 2026)},
  pages =	{10:1--10:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-420-8},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{369},
  editor =	{Bille, Philip 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.CPM.2026.10},
  URN =		{urn:nbn:de:0030-drops-259361},
  doi =		{10.4230/LIPIcs.CPM.2026.10},
  annote =	{Keywords: Supermaximal repeats, Largest maximal repeats, Net frequencies, Run-length Burrows-Wheeler transform, Compressed data mining}
}
Document
DOI: 10.4230/LIPIcs.SoCG.2026.54
Approximating Pareto Sum via Bounded Monotone Min-Plus Convolution

Authors: Geri Gokaj, Marvin Künnemann, Sabine Storandt, and Carina Truschel

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

Abstract
The Pareto sum of two-dimensional point sets P and Q in ℝ² is defined as the skyline of the points in their Minkowski sum. The problem of efficiently computing the Pareto sum arises frequently in bi-criteria optimization algorithms. Prior work establishes that computing the Pareto sum of sets P and Q of size n suffers from conditional lower bounds that rule out strongly subquadratic O(n^{2-ε})-time algorithms, even when the output size is Θ(n). Naturally, we ask: How efficiently can we approximate Pareto sums, both in theory and practice? Can we beat the near-quadratic-time state of the art for exact algorithms? On the theoretical side, we formulate a notion of additively approximate Pareto sets and show that computing an approximate Pareto set is fine-grained equivalent to Bounded Monotone Min-Plus Convolution. Leveraging a remarkable Õ(n^{1.5})-time algorithm for the latter problem (Chi, Duan, Xie, Zhang; STOC '22), we thus obtain a strongly subquadratic (and conditionally optimal) approximation algorithm for computing Pareto sums. On the practical side, we engineer different algorithmic approaches for approximating Pareto sets on realistic instances. Our implementations enable a granular trade-off between approximation quality and running time/output size compared to the state of the art for exact algorithms established in (Funke, Hespe, Sanders, Storandt, Truschel; Algorithmica '25). Perhaps surprisingly, the (theoretical) connection to Bounded Monotone Min-Plus Convolution remains beneficial even for our implementations: in particular, we implement a simplified, yet still subquadratic version of an algorithm due to Chi, Duan, Xie and Zhang, which on some sufficiently large instances outperforms the competing quadratic-time approaches.
Cite as

Geri Gokaj, Marvin Künnemann, Sabine Storandt, and Carina Truschel. Approximating Pareto Sum via Bounded Monotone Min-Plus Convolution. In 42nd International Symposium on Computational Geometry (SoCG 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 367, pp. 54:1-54:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{gokaj_et_al:LIPIcs.SoCG.2026.54,
  author =	{Gokaj, Geri and K\"{u}nnemann, Marvin and Storandt, Sabine and Truschel, Carina},
  title =	{{Approximating Pareto Sum via Bounded Monotone Min-Plus Convolution}},
  booktitle =	{42nd International Symposium on Computational Geometry (SoCG 2026)},
  pages =	{54:1--54:21},
  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.54},
  URN =		{urn:nbn:de:0030-drops-258602},
  doi =		{10.4230/LIPIcs.SoCG.2026.54},
  annote =	{Keywords: computational geometry, fine-grained complexity, algorithm engineering}
}
Document
Short Paper
DOI: 10.4230/OASIcs.FMBC.2026.9
Towards Property-Based Testing of Smart Contracts Using Gas Analysis (Short Paper)

Authors: Elvira Albert, Emanuele De Angelis, Marco Di Ianni, Fabio Fioravanti, and Pablo Gordillo

Published in: OASIcs, Volume 142, 7th International Workshop on Formal Methods for Blockchains (FMBC 2026)

Abstract
Testing has become an integral part of the software development process in order to ensure the correct and safe execution of programs. A powerful approach to testing is property-based testing that aims at generating unit tests that verify that a certain property of interest holds. However, smart contracts are also characterized by important non-functional aspects, such as the gas consumption required to execute their functions. Static gas analyzers are able to obtain parametric gas bounds - that soundly over-approximate - the gas consumption of executing each of the public functions within a smart contract. This paper discusses our ideas towards combining both formal methods, property-based testing and gas analysis, in order to generate gas-aware unit tests that can ensure the gas requirements provided by the programmers.
Cite as

Elvira Albert, Emanuele De Angelis, Marco Di Ianni, Fabio Fioravanti, and Pablo Gordillo. Towards Property-Based Testing of Smart Contracts Using Gas Analysis (Short Paper). In 7th International Workshop on Formal Methods for Blockchains (FMBC 2026). Open Access Series in Informatics (OASIcs), Volume 142, pp. 9:1-9:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{albert_et_al:OASIcs.FMBC.2026.9,
  author =	{Albert, Elvira and De Angelis, Emanuele and Di Ianni, Marco and Fioravanti, Fabio and Gordillo, Pablo},
  title =	{{Towards Property-Based Testing of Smart Contracts Using Gas Analysis}},
  booktitle =	{7th International Workshop on Formal Methods for Blockchains (FMBC 2026)},
  pages =	{9:1--9:8},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-424-6},
  ISSN =	{2190-6807},
  year =	{2026},
  volume =	{142},
  editor =	{Bartoletti, Massimo and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2026.9},
  URN =		{urn:nbn:de:0030-drops-257069},
  doi =		{10.4230/OASIcs.FMBC.2026.9},
  annote =	{Keywords: Property-based Testing, Blockchain, Ethereum, Gas}
}
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.17
Don’t Get Caught, Keep Your Onions in a Vault

Authors: Humza Ikram, Rumaisa Habib, Muaz Ali, and Zartash Afzal Uzmi

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

Abstract
When web applications wish to operate anonymously, they routinely host themselves as "Hidden Services" in the Tor network. However, these services are frequently threatened by deanonymization attacks, whereby their IP address and location may be inferred by the authorities. We present VaulTor, a novel architecture for the Tor network that ensures an extra layer of security for the Hidden Services against deanonymization attacks. In this new architecture, a volunteer (vault) is incentivized to host the web application content on behalf of the Hidden Service. The vault runs the hosted application in a Trusted Execution Environment (TEE) and becomes the point of contact for interested clients. This setup can substantially reduce the uptime requirement of the original Hidden Service provider, thereby significantly decreasing the chance of deanonymization attacks against them. Using a vault node in place of the hidden service node does not cause any noticeable performance degradation when accessing the hosted content.
Cite as

Humza Ikram, Rumaisa Habib, Muaz Ali, and Zartash Afzal Uzmi. Don’t Get Caught, Keep Your Onions in a Vault. In 1st New Ideas in Networked Systems (NINeS 2026). Open Access Series in Informatics (OASIcs), Volume 139, pp. 17:1-17:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{ikram_et_al:OASIcs.NINeS.2026.17,
  author =	{Ikram, Humza and Habib, Rumaisa and Ali, Muaz and Uzmi, Zartash Afzal},
  title =	{{Don’t Get Caught, Keep Your Onions in a Vault}},
  booktitle =	{1st New Ideas in Networked Systems (NINeS 2026)},
  pages =	{17:1--17:24},
  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.17},
  URN =		{urn:nbn:de:0030-drops-256027},
  doi =		{10.4230/OASIcs.NINeS.2026.17},
  annote =	{Keywords: Tor, anonymity, Hidden Services, Trusted Execution Environments}
}
Document
DOI: 10.4230/OASIcs.NINeS.2026.18
TURBO: Utility-Aware Bandwidth Allocation for Cloud-Augmented Autonomous Control

Authors: Peter Schafhalter, Alexander Krentsel, Hongbo Wei, Joseph E. Gonzalez, Sylvia Ratnasamy, Scott Shenker, and Ion Stoica

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

Abstract
Autonomous driving system progress has been driven by improvements in machine learning (ML) models, whose computational demands now exceed what edge devices alone can provide. The cloud offers abundant compute, but the network has long been treated as an unreliable bottleneck rather than a co-equal part of the autonomous vehicle control loop. We argue that this separation is no longer tenable: safety-critical autonomy requires co-design of control, models, and network resource allocation itself. We introduce TURBO, a cloud-augmented control framework that addresses this challenge, formulating bandwidth allocation and control pipeline configuration across both the car and cloud as a joint optimization problem. TURBO maximizes benefit to the car while guaranteeing safety in the face of highly variable network conditions. We implement TURBO and evaluate it in both simulation and real-world deployment, showing it can improve average accuracy by up to 15.6%pt over existing on-vehicle-only pipelines. Our code is made available at www.github.com/NetSys/turbo.
Cite as

Peter Schafhalter, Alexander Krentsel, Hongbo Wei, Joseph E. Gonzalez, Sylvia Ratnasamy, Scott Shenker, and Ion Stoica. TURBO: Utility-Aware Bandwidth Allocation for Cloud-Augmented Autonomous Control. In 1st New Ideas in Networked Systems (NINeS 2026). Open Access Series in Informatics (OASIcs), Volume 139, pp. 18:1-18:34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{schafhalter_et_al:OASIcs.NINeS.2026.18,
  author =	{Schafhalter, Peter and Krentsel, Alexander and Wei, Hongbo and Gonzalez, Joseph E. and Ratnasamy, Sylvia and Shenker, Scott and Stoica, Ion},
  title =	{{TURBO: Utility-Aware Bandwidth Allocation for Cloud-Augmented Autonomous Control}},
  booktitle =	{1st New Ideas in Networked Systems (NINeS 2026)},
  pages =	{18:1--18:34},
  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.18},
  URN =		{urn:nbn:de:0030-drops-256039},
  doi =		{10.4230/OASIcs.NINeS.2026.18},
  annote =	{Keywords: autonomous vehicles, bandwidth allocation, cloud computing, edge computing, machine learning}
}
Document
DOI: 10.4230/LIPIcs.STACS.2026.37
Random Models and Guarded Logic

Authors: Oskar Fiuk

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)

Abstract
Building on ideas of Gurevich and Shelah for the Gödel Class, we present a new probabilistic proof of the finite model property for the Guarded Fragment of First-Order Logic. Our proof is conceptually simple and yields the optimal doubly-exponential upper bound on the size of minimal models. We precisely analyse the obtained bound, up to constant factors in the exponents, and construct sentences that enforce models of tightly matching size. The probabilistic approach adapts naturally to the Triguarded Fragment, an extension of the Guarded Fragment that also subsumes the Two-Variable Fragment. Finally, we derandomise the probabilistic proof by providing an explicit model construction which replaces randomness with deterministic hash functions.
Cite as

Oskar Fiuk. Random Models and Guarded Logic. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 37:1-37:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{fiuk:LIPIcs.STACS.2026.37,
  author =	{Fiuk, Oskar},
  title =	{{Random Models and Guarded Logic}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{37:1--37:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.37},
  URN =		{urn:nbn:de:0030-drops-255269},
  doi =		{10.4230/LIPIcs.STACS.2026.37},
  annote =	{Keywords: guarded fragment, finite model property, probabilistic method}
}
Document
DOI: 10.4230/LIPIcs.STACS.2026.14
Computing Tarski Fixed Points in Financial Networks

Authors: Leander Besting, Martin Hoefer, and Lars Huth

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)

Abstract
Modern financial networks are highly connected and result in complex interdependencies of the involved institutions. In the prominent Eisenberg-Noe model [Eisenberg and Noe, 2001], a fundamental aspect is clearing - to determine the amount of assets available to each financial institution in the presence of potential defaults and bankruptcy. A clearing state represents a fixed point that satisfies a set of natural axioms. Existence can be established (even in broad generalizations of the model) using Tarski’s theorem. While a maximal fixed point can be computed in polynomial time, the complexity of computing other fixed points is open. In this paper, we provide an efficient algorithm to compute a minimal fixed point. Our algorithm applies in a broad generalization of the Eisenberg-Noe model with any monotone, piecewise-linear payment functions and default costs. We also study claims trading, a local network adjustment to improve clearing, when networks are evaluated with minimal clearing. We provide an efficient algorithm to decide existence of Pareto-improving trades and compute optimal ones if they exist.
Cite as

Leander Besting, Martin Hoefer, and Lars Huth. Computing Tarski Fixed Points in Financial Networks. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{besting_et_al:LIPIcs.STACS.2026.14,
  author =	{Besting, Leander and Hoefer, Martin and Huth, Lars},
  title =	{{Computing Tarski Fixed Points in Financial Networks}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{14:1--14:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.14},
  URN =		{urn:nbn:de:0030-drops-255038},
  doi =		{10.4230/LIPIcs.STACS.2026.14},
  annote =	{Keywords: Tarski Fixed Points, Financial Networks, Minimal Clearing, Claims Trade}
}
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.CSL.2026.48
Interpreting Lambda Calculus in Domain-Valued Random Variables

Authors: Robert Furber, Radu Mardare, Prakash Panangaden, and Dana Scott

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

Abstract
We develop Boolean-valued domain theory and show how the lambda-calculus can be interpreted using domain-valued random variables. We focus on the reflexive domain construction rather than the language and its semantics. We develop the Boolean-valued set theory needed from scratch and then develop Boolean-valued domain theory on top of that. The notions of equality and partial order have to be given Boolean-valued interpretations; when we say that an equation is valid in the model we mean that its interpretation is the top element of the Boolean algebra.
Cite as

Robert Furber, Radu Mardare, Prakash Panangaden, and Dana Scott. Interpreting Lambda Calculus in Domain-Valued Random Variables. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 48:1-48:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{furber_et_al:LIPIcs.CSL.2026.48,
  author =	{Furber, Robert and Mardare, Radu and Panangaden, Prakash and Scott, Dana},
  title =	{{Interpreting Lambda Calculus in Domain-Valued Random Variables}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{48:1--48:20},
  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.48},
  URN =		{urn:nbn:de:0030-drops-254734},
  doi =		{10.4230/LIPIcs.CSL.2026.48},
  annote =	{Keywords: lambda calculus, domain theory, random variables}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.15
Cyclic Proof Theory of Generalised Inductive Definitions

Authors: Gianluca Curzi and Lukas Melgaard

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

Abstract
We study cyclic proof systems for μPA, an extension of Peano arithmetic by generalised inductive definitions that is arithmetically equivalent to the (impredicative) subsystem of second-order arithmetic Π^1_2-CA₀ by Möllerfeld. The main result of this paper is that cyclic and inductive μPA have the same proof-theoretic strength. First, we translate cyclic proofs into an annotated variant based on Sprenger and Dam’s systems for first-order μ-calculus, whose stronger validity condition allows for a simpler proof of soundness. We then formalise this argument within Π^1_2-CA₀, leveraging Möllerfeld’s conservativity properties. To this end, we build on prior work by Curzi and Das on the reverse mathematics of the Knaster-Tarski theorem. As a byproduct of our proof methods we show that, despite the stronger validity condition, annotated and "plain" cyclic proofs for μPA prove the same theorems. This work represents a further step in the non-wellfounded proof-theoretic analysis of theories of arithmetic via impredicative fragments of second-order arithmetic, an approach initiated by Simpson’s Cyclic Arithmetic, and continued by Das and Melgaard in the context of arithmetical inductive definitions.
Cite as

Gianluca Curzi and Lukas Melgaard. Cyclic Proof Theory of Generalised Inductive Definitions. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 15:1-15:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{curzi_et_al:LIPIcs.CSL.2026.15,
  author =	{Curzi, Gianluca and Melgaard, Lukas},
  title =	{{Cyclic Proof Theory of Generalised Inductive Definitions}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{15:1--15:19},
  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.15},
  URN =		{urn:nbn:de:0030-drops-254399},
  doi =		{10.4230/LIPIcs.CSL.2026.15},
  annote =	{Keywords: cyclic proofs, positive inductive definitions, arithmetic, fixed points, proof theory, reset proof systems}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.23
A Logic for Fresh Labelled Transition Systems

Authors: Mohamed H. Bandukara and Nikos Tzevelekos

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

Abstract
We introduce a Hennessy-Milner logic with recursion for Fresh Labelled Transition Systems (FLTSs). These are nominal labelled transition systems which keep track of the history, i.e. of data values seen so far, and can model fresh data generation. In particular, FLTSs generalise the computations of Fresh-Register Automata, which in turn can be seen as a "regular" class of history-tracking automata operating on infinite input alphabets. The logic we introduce is a modal mu-calculus equipped with infinite disjunctions over arbitrary and fresh data values respectively, while its recursion is parameterised on vectors of data values. It can express a variety of properties, such as the existence of an infinite path of distinct data values, the absence of paths where values are repeated, or the existence of a finite path where some taint property is violated. We study the model-checking problem and its complexity via a reduction to parity games and, using nominal sets techniques, provide an exponential upper bound for it.
Cite as

Mohamed H. Bandukara and Nikos Tzevelekos. A Logic for Fresh Labelled Transition Systems. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 23:1-23:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bandukara_et_al:LIPIcs.CSL.2026.23,
  author =	{Bandukara, Mohamed H. and Tzevelekos, Nikos},
  title =	{{A Logic for Fresh Labelled Transition Systems}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{23:1--23: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.23},
  URN =		{urn:nbn:de:0030-drops-254478},
  doi =		{10.4230/LIPIcs.CSL.2026.23},
  annote =	{Keywords: Nominal Transition Systems, Hennessy-Milner Logic, Modal Mu-Calculus, Register Automata, Nominal Sets, Parity Games}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.40
The Groupoid-Syntax of Type Theory Is a Set

Authors: Thorsten Altenkirch, Ambrus Kaposi, and Szumi Xie

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

Abstract
Categories with families (CwFs) have been used to define the semantics of type theory in type theory. In the setting of Homotopy Type Theory (HoTT), one of the limitations of the traditional notion of CwFs is the requirement to set-truncate types, which excludes models based on univalent categories, such as the standard set model. To address this limitation, we introduce the concept of a Groupoid Category with Families (GCwF). This framework truncates types at the groupoid level and incorporates coherence equations, providing a natural extension of the CwF framework when starting from a 1-category. We demonstrate that the initial GCwF for a type theory with a base family of sets and Π-types (groupoid-syntax) is set-truncated. Consequently, this allows us to utilize the conventional intrinsic syntax of type theory while enabling interpretations in semantically richer and more natural models. All constructions in this paper were formalised in Cubical Agda.
Cite as

Thorsten Altenkirch, Ambrus Kaposi, and Szumi Xie. The Groupoid-Syntax of Type Theory Is a Set. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 40:1-40:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{altenkirch_et_al:LIPIcs.CSL.2026.40,
  author =	{Altenkirch, Thorsten and Kaposi, Ambrus and Xie, Szumi},
  title =	{{The Groupoid-Syntax of Type Theory Is a Set}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{40:1--40:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.40},
  URN =		{urn:nbn:de:0030-drops-254650},
  doi =		{10.4230/LIPIcs.CSL.2026.40},
  annote =	{Keywords: Categorical models of type theory, category with families, groupoids, coherence, homotopy type theory}
}
  • Refine by Type
  • 126 Document/PDF
  • 116 Document/HTML

  • Refine by Publication Year
  • 20 2026
  • 93 2025
  • 3 2024
  • 3 2023
  • 1 2022
  • Show More...

  • Refine by Author
  • 3 Kamburjan, Eduard
  • 2 Accattoli, Beniamino
  • 2 Albouy, Timothé
  • 2 Bolz-Tereick, Carl Friedrich
  • 2 Choudhary, Keerti
  • Show More...

  • Refine by Series/Journal
  • 105 LIPIcs
  • 10 OASIcs
  • 3 LITES
  • 8 TGDK

  • Refine by Classification
  • 11 Theory of computation → Logic and verification
  • 8 Theory of computation → Type theory
  • 6 Theory of computation → Lambda calculus
  • 6 Theory of computation → Regular languages
  • 5 Software and its engineering → Formal software verification
  • Show More...

  • Refine by Keyword
  • 3 Isabelle/HOL
  • 3 Quantum Circuits
  • 3 Verification
  • 2 Active Objects
  • 2 Bidirectional typing
  • 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