Demo Data from VLDB 2026 / reviewers in the wild / expert
Lucas Kehrer
dblp:436/6538
· DBLP profile ↗
1ranked-venue papers
0as first author
1since 2021 · last 2026
—ORCID · unresolved
Domains — the database's venue-derived domains; a paper can count in several
Theory of computation · 1 · 1 since 2021
Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.
| Theoretical computer science
1 paper |
Logic in computer science · 100% | |
| Software engineering, system software, and programming languages
1 paper |
Program verification · 100% |
Topics — the 5 heaviest of 5, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Program verification › model checking
k-induction |
1.0 | 1 | 2026 | The Algebra of Iterative Constructions · LICS 2026 |
Logic in computer science
algebraic logic |
1.0 | 1 | 2026 | The Algebra of Iterative Constructions · LICS 2026 |
Logic in computer science › algebraic logic
equational logic |
1.0 | 1 | 2026 | The Algebra of Iterative Constructions · LICS 2026 |
Logic in computer science › domain theory
fixed points |
1.0 | 1 | 2026 | The Algebra of Iterative Constructions · LICS 2026 |
Logic in computer science › domain theory › fixed points
fixed point theorem |
1.0 | 1 | 2026 | The Algebra of Iterative Constructions · LICS 2026 |
Methods — techniques the papers use, named apart from their topics
sledgehammer · 2.0mechanized proof · 2.0Isabelle/HOL · 2.0
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2026 | The Algebra of Iterative ConstructionsabstractFixed points are a recurring theme in computer science and are often constructed as limits of suitably seeded fixed point iterations. We present the algebra of iterative constructions (AIC) - a purely algebraic approach to reasoning about fixed point iterations of continuous endomaps on complete lattices. AIC allows derivations of constructive fixed point theorems via equational logic and avoids explicit computations with indices. For example, F ◇ F^* ⊥ = ◇ F^* ⊥ states in AIC that sup_n Fⁿ (⊥) - a construction known from the Kleene fixed point theorem - is a fixed point of F. We demonstrate the applicability of AIC by providing algebraic proofs of several well- and less-well-known fixed point theorems: Among others, we prove the Tarski-Kantorovich principle - a generalization of the Kleene fixed point theorem - as well as a fixed point-theoretic generalization of k-induction - a technique used in software verification. We moreover present a novel fixed point theorem. It improves a recent generalization of the Tarski-Kantorovich principle due to Olszewski for obtaining pre- and postfixed points from lattice-theoretic limit inferiors and limit superiors through iterating an endomap on an arbitrary seed element: We identify sufficient continuity conditions on the endomaps so that these limits become proper fixed points. We have mechanized our algebra in Isabelle/HOL. Isabelle’s sledgehammer tool is able to find proofs of the above fixed point theorems fully automatically. Finally, we investigate the completeness of our axiomatization of AIC. We prove that our finite set of finitary axioms is (a) sound but incomplete for standard models of AIC (sequences of elements from a complete lattice) and that (b) a different finite set of infinitary axioms is complete. We also prove that infinitary axioms are unavoidable: there exists no complete axiomatization of standard models given by finitely many finitary axioms. Kevin Batz, Benjamin Lucien Kaminski, Lucas Kehrer, Gerwin Klein, Todd Schmid, Henning Urbat |
LICS | 3 |