VLDB 2026 Research / reviewers in the wild / expert
Andrew Kenyon-Roberts
dblp:286/1043
· DBLP profile ↗
1ranked-venue papers
1as first author
1since 2021 · last 2021
—ORCID · none
Domains — the database's venue-derived domains; a paper can count in several
Theory of computation · 1 · 1 first-author · 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 |
Automated reasoning and model checking · 61% Logic in computer science · 39% |
Topics — the 3 heaviest of 4, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Automated reasoning and model checking › probabilistic verification
almost-sure termination |
0.5 | 1 | 2021 | Supermartingales, Ranking Functions and Probabilistic Lambda Calculus · LICS 2021 |
Automated reasoning and model checking
program verification |
0.5 | 1 | 2021 | Supermartingales, Ranking Functions and Probabilistic Lambda Calculus · LICS 2021 |
Logic in computer science
semantics |
0.5 | 1 | 2021 | Supermartingales, Ranking Functions and Probabilistic Lambda Calculus · LICS 2021 |
Methods — techniques the papers use, named apart from their topics
sparse ranking functions · 0.5ranking supermartingales · 0.5antitone ranking functions · 0.5
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2021 | Supermartingales, Ranking Functions and Probabilistic Lambda CalculusabstractWe introduce a method for proving almost sure termination in the context of lambda calculus with continuous random sampling and explicit recursion, based on ranking supermartingales. This result is extended in three ways. Antitone ranking functions have weaker restrictions on how fast they must decrease, and are applicable to a wider range of programs. Sparse ranking functions take values only at a subset of the program's reachable states, so they are simpler to define and more flexible. Ranking functions with respect to alternative reduction strategies give yet more flexibility, and significantly increase the applicability of the ranking supermartingale approach to proving almost sure termination, thanks to a novel (restricted) confluence result which is of independent interest. The notion of antitone ranking function was inspired by similar work by McIver, Morgan, Kaminski and Katoen in the setting of a first-order imperative language, but adapted to a higher-order functional language. The sparse ranking function and confluent semantics extensions are unique to the higher-order setting. Our methods can be used to prove almost sure termination of programs that are beyond the reach of methods in the literature, including higher-order and non-affine recursion. Andrew Kenyon-Roberts, C.-H. Luke Ong |
LICS | 1 |