23 citations · 24 across the 8 of their papers we have counts for
8 papers
Efficient Cost Bounds with Linear Maps
David M Kahn, Jan Hoffmann, Thomas Reps +1
The Automatic Amortized Resource Analysis (AARA) derives program-execution cost bounds using types. To do so, AARA often makes use of cost-free types, which are critical for the co…
Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment
David M Kahn, Jan Hoffmann, Runming Li
As is evident in the programming language literature, many practitioners favor specifying dynamic program behavior using big-step over small-step semantics. Unlike small-step seman…
Automatic Amortized Resource Analysis with Regular Recursive Types
Jessie Grosen, David M. Kahn, Jan Hoffmann
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 automa…
Automatic Amortized Resource Analysis with the Quantum Physicist's Method
David M Kahn, Jan Hoffmann
We present a novel method for working with the physicist's method of amortized resource analysis, which we call the quantum physicist's method. These principles allow for more prec…
Raising Expectations: Automating Expected Cost Analysis with Types
Di Wang, David M Kahn, Jan Hoffmann
This article presents a type-based analysis for deriving upper bounds on the expected execution cost of probabilistic programs. The analysis is naturally compositional, parametric…
Exponential Automatic Amortized Resource Analysis
David M Kahn, Jan Hoffmann
Automatic amortized resource analysis (AARA) is a type-based technique for inferring concrete (non-asymptotic) bounds on a program's resource usage. Existing work on AARA has focus…