Jessie Grosen

dblp:345/8246 · DBLP profile ↗
← Back
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

TopicWeightPapersLastEvidence papers
Program analysis › resource analysis › amortized analysis
automatic amortized resource analysis
0.712023
Automatic Amortized Resource Analysis with Regular Recursive Types · LICS 2023
Programming languages and type systems › type systems
recursive types
0.712023
Automatic Amortized Resource Analysis with Regular Recursive Types · LICS 2023
Program analysis
resource analysis
0.712023
Automatic Amortized Resource Analysis with Regular Recursive Types · LICS 2023
Programming languages and type systems
type systems
0.712023
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
YearPublicationVenuePosition
2023 Automatic Amortized Resource Analysis with Regular Recursive Types
abstract
The 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
LICS1