EDBT 2026 Demo / reviewers in the wild / expert
Jessie Grosen
dblp:345/8246
· DBLP profile ↗
1ranked-venue papers
1as first author
1since 2021 · last 2023
—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.
| Software engineering, system software, and programming languages
1 paper |
Programming languages and type systems · 50% Program analysis · 50% |
Topics — the 4 heaviest of 4, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Program analysis › resource analysis › amortized analysis
automatic amortized resource analysis |
0.7 | 1 | 2023 | Automatic Amortized Resource Analysis with Regular Recursive Types · LICS 2023 |
Programming languages and type systems › type systems
recursive types |
0.7 | 1 | 2023 | Automatic Amortized Resource Analysis with Regular Recursive Types · LICS 2023 |
Program analysis
resource analysis |
0.7 | 1 | 2023 | Automatic Amortized Resource Analysis with Regular Recursive Types · LICS 2023 |
Programming languages and type systems
type systems |
0.7 | 1 | 2023 | Automatic Amortized Resource Analysis with Regular Recursive Types · LICS 2023 |
Methods — techniques the papers use, named apart from their topics
semimodules · 0.7logical relations · 0.7amortized analysis · 0.7
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2023 | Automatic Amortized Resource Analysis with Regular Recursive TypesabstractThe goal of automatic resource bound analysis is to statically infer symbolic bounds on the resource consumption of the evaluation of a program. A longstanding challenge for automatic resource analysis is the inference of bounds that are functions of complex custom data structures. This article builds on type-based automatic amortized resource analysis (AARA) to address this challenge. AARA is based on the potential method of amortized analysis and reduces bound inference to standard type inference with additional linear constraint solving, even when deriving non-linear bounds. Such bounds come from resource functions, which are linear combinations of basic functions of data structure sizes that fulfill certain closure properties.Previous work on AARA defined resource functions for many data structures such as lists of lists, but left open whether such functions exist for arbitrary data structures. This work answers this question positively by uniformly constructing resource polynomials for algebraic data structures defined by regular recursive types. These functions are a generalization of all previously proposed polynomial resource functions and can be seen as a general notion of polynomials for values of a given recursive type. A resource type system for FPC, a core language with recursive types, demonstrates how resource polynomials can be integrated with AARA while preserving all benefits of past techniques. The article also proposes the use of new techniques useful for stating the rules of this type system succinctly and proving it sound against a small-step cost semantics. First, multivariate potential annotations are stated in terms of free semimodules, substantially abstracting details of the presentation of annotations and the proofs of their properties. Second, a logical relation giving semantic meaning to resource types enables a proof of soundness by a single induction on typing derivations. Jessie Grosen, David M. Kahn, Jan Hoffmann 0002 |
LICS | 1 |