Publications (28)
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…
Verifying and Synthesizing Constant-Resource Implementations with Types
Van Chan Ngo, Mario Dehesa-Azuara, Matthew Fredrikson +1
We propose a novel type system for verifying that programs correctly implement constant-resource behavior. Our type system extends recent work on automatic amortized resource analy…
The Complexity of Computing Minimal Unidirectional Covering Sets
Dorothea Baumeister, Felix Brandt, Felix Fischer +2
Given a binary dominance relation on a set of alternatives, a common thread in the social sciences is to identify subsets of alternatives that satisfy certain notions of stability.…
Sound Probabilistic Inference via Guide Types
Di Wang, Jan Hoffmann, Thomas Reps
Probabilistic programming languages aim to describe and automate Bayesian modeling and inference. Modern languages support programmable inference, which allows users to customize i…
Work Analysis with Resource-Aware Session Types
Ankush Das, Jan Hoffmann, Frank Pfenning
While there exist several successful techniques for supporting programmers in deriving static resource bounds for sequential code, analyzing the resource usage of message-passing c…
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…
LFPL: Revisited and Mechanized
Nathaniel Glover, Jan Hoffmann
Hofmann (1999) introduced the functional programming language LFPL to characterize the functions computable in polynomial time using an affine type system. LFPL enables a natural p…
Probabilistic Resource-Aware Session Types
Ankush Das, Di Wang, Jan Hoffmann
Session types guarantee that message-passing processes adhere to predefined communication protocols. Prior work on session types has focused on deterministic languages but many mes…
Potential Functions as Types
Harrison Grodin, Ethan Chu, Runming Li +2
Amortized analysis can be framed from the physicist's view, amenable to manual verification in dependent type theory using potential functions, and the banker's view, amenable to a…
Central Moment Analysis for Cost Accumulators in Probabilistic Programs
Di Wang, Jan Hoffmann, Thomas Reps
For probabilistic programs, it is usually not possible to automatically derive exact information about their properties, such as the distribution of states at a given program point…
Bounded Expectations: Resource Analysis for Probabilistic Programs
Van Chan Ngo, Quentin Carbonneaux, Jan Hoffmann
This paper presents a new static analysis for deriving upper bounds on the expected resource consumption of probabilistic programs. The analysis is fully automatic and derives symb…
Tracking Data-Flow with Open Closure Types
Gabriel Scherer, Jan Hoffmann
Type systems hide data that is captured by function closures in function types. In most cases this is a beneficial design that favors simplicity and compositionality. However, some…
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…
Resource-Aware Session Types for Digital Contracts
Ankush Das, Stephanie Balzer, Jan Hoffmann +2
Programming digital contracts comes with unique challenges, which include (i) expressing and enforcing protocols of interaction, (ii) controlling resource usage, and (iii) preventi…
Towards Automatic Resource Bound Analysis for OCaml
Jan Hoffmann, Ankush Das, Shu-Chun Weng
This article presents a resource analysis system for OCaml programs. This system automatically derives worst-case resource bounds for higher-order polymorphic programs with user-de…
Liquid Resource Types
Tristan Knoth, Di Wang, Adam Reynolds +2
This article presents liquid resource types, a technique for automatically verifying the resource consumption of functional programs. Existing resource analysis techniques trade au…
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…
Expected-Cost Analysis for Probabilistic Programs and Semantics-Level Adaption of Optional Stopping Theorems
Di Wang, Jan Hoffmann, Thomas Reps
In this article, we present a semantics-level adaption of the Optional Stopping Theorem, sketch an expected-cost analysis as its application, and survey different variants of the O…
Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
Samuel R. Buss, Jan Hoffmann, Jan Johannsen
Resolution refinements called w-resolution trees with lemmas (WRTL) and with input lemmas (WRTI) are introduced. Dag-like resolution is equivalent to both WRTL and WRTI when there…
Typable Fragments of Polynomial Automatic Amortized Resource Analysis
Long Pham, Jan Hoffmann
Being a fully automated technique for resource analysis, automatic amortized resource analysis (AARA) can fail in returning worst-case cost bounds of programs, fundamentally due to…
Parallel Complexity Analysis with Temporal Session Types
Ankush Das, Jan Hoffmann, Frank Pfenning
We study the problem of parametric parallel complexity analysis of concurrent, message-passing programs. To make the analysis local and compositional, it is based on a conservative…
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…
Proceedings 16th International Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software
Farzaneh Derakhshan, Jan Hoffmann
This volume contains the proceedings of PLACES 2025, the 16th edition of the Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software. The work…
Worst-Case Input Generation for Concurrent Programs under Non-Monotone Resource Metrics
Long Pham, Jan Hoffmann
Worst-case input generation aims to automatically generate inputs that exhibit the worst-case performance of programs. It has several applications, and can, for example, detect vul…
From Dust to Planets -- A Chemical Perspective
Klaus Mezger, Jonas Pape, Aryavart Anand +3
Chemical and chronological information preserved in meteorites permits the reconstruction of events and processes in the solar nebula from the formation of the first solids to the…
Handling Exceptions and Effects with Automatic Resource Analysis
Ethan Chu, Yiyang Guo, Jan Hoffmann
There exist many techniques for automatically deriving parametric resource (or cost) bounds by analyzing the source code of a program. These techniques work effectively for a large…
Resource-Guided Program Synthesis
Tristan Knoth, Di Wang, Nadia Polikarpova +1
This article presents resource-guided synthesis, a technique for synthesizing recursive programs that satisfy both a functional specification and a symbolic resource bound. The tec…