publications
Publications in reversed chronological order.
2026
-
Big-Stop Semantics
David Kahn,
Runming Li,
and Jan Hoffmann
In 53rd Symposium on Principles of Programming Languages (POPL ’26).
2026
[pdf]
2025
-
Integrating Resource Analyses via Resource Decomposition
Long Pham,
Yue Niu,
Nathan Glover,
Feras Saad,
and Jan Hoffmann
In Conference on Object-Oriented Programming Systems,
Languages, and Applications (OOPSLA’25).
2025
[pdf]
-
Handling Exceptions and Algebraic Effects with Automatic Resource Analysis
Ethan Chu,
Yiyang Guo,
and Jan Hoffmann
Working paper.
2025
2024
-
Worst-Case Input Generation for Concurrent Programs under Non-Monotone Resource Metrics
Long Pham,
and Jan Hoffmann
Logical Methods in Computer Science.
2024
[pdf]
-
Programmable MCMC with Soundly Composed Guide Programs
Long Pham,
Di Wang,
Feras Saad,
and Jan Hoffmann
In Conference on Object-Oriented Programming Systems,
Languages, and Applications (OOPSLA’24).
2024
[pdf]
[tr]
-
Robust Resource Bounds with Static Analysis and Bayesian Inference
Long Pham,
Feras A. Saad,
and Jan Hoffmann
In 45th Conference on Programming Language Design and
Implementation (PLDI’24).
2024
[pdf]
[tr]
-
-
Modeling and Analyzing Evaluation Cost of CUDA Kernels
Stefan Muller,
and Jan Hoffmann
ACM Transactions on Parallel Computing.
2024
[pdf]
2023
-
Nomos-UC: A Programming Framework for Cryptography Based on Resource-Aware Session Types
Surya Bakshi,
Ankush Das,
Andrew Miller,
and Jan Hoffmann
Working paper.
2023
-
Automatic Amortized Resource Analysis with Regular Recursive Types
Jessie Grosen,
David Kahn,
and Jan Hoffmann
In 38th ACM/IEEE Symposium on Logic in Computer Science (LICS’ 23).
2023
[pdf]
[tr]
-
Worst-Case Input Generation for Concurrent Processes
Long Pham,
and Jan Hoffmann
Working paper.
2023
-
Probabilistic Resource-Aware Session Types
Ankush Das,
Di Wang,
and Jan Hoffmann
In 50th Symposium on Principles of Programming Languages (POPL ’23).
2023
[pdf]
[tr]
2022
-
Nomos: A Protocol-Enforcing, Asset-Tracking, and Gas-Aware Language for Smart Contracts
Ankush Das,
Jan Hoffmann,
and Frank Pfenning
Technical Report.
2022
[pdf]
-
Two Decades of Automatic Amortized Resource Analysis
Jan Hoffmann,
and Steffen Jost
Math. Struct. Comput. Sci..
2022
[pdf]
2021
-
Automatic Resource Analysis with the Quantum Physicist’s Method
David Kahn,
and Jan Hoffmann
In 26th International Conference on Functional Programming (ICFP’21).
2021
[pdf]
-
Central Moment Analysis for Cost Accumulators in Probabilistic Programs
Di Wang,
Jan Hoffmann,
and Thomas Reps
In 42th Conference on Programming Language Design and Implementation (PLDI’21).
2021
[pdf]
-
Sound Probabilistic Inference via Guide Types
Di Wang,
Jan Hoffmann,
and Thomas Reps
In 42th Conference on Programming Language Design and Implementation (PLDI’21).
2021
[pdf]
-
Modeling and Analyzing Evaluation Cost of CUDA Kernels
Stefan Muller,
and Jan Hoffmann
In 48th Symposium on Principles of Programming Languages (POPL’21).
2021
[pdf]
-
A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis
Vineet Rajani,
Marco Gaboardi,
Deepak Garg,
and Jan Hoffmann
In 48th Symposium on Principles of Programming Languages (POPL’21).
2021
[pdf]
-
Typable Fragments of Polynomial Automatic Amortized Resource Analysis
Long Pham,
and Jan Hoffmann
In 29th EACSL Annual Conference on Computer Science Logic (CSL’21).
2021
[pdf]
-
2020
-
Combining Source and Target Level Cost Analyses for OCaml Programs
Stefan Muller,
and Jan Hoffmann
Working paper.
2020
[pdf]
-
Liquid Resource Types
Tristan Knoth,
Di Wang,
Adam Reynolds,
Nadia Polikarpova,
and Jan Hoffmann
In 25th International Conference on Functional Programming (ICFP’20).
2020
[pdf]
-
Raising Expectations: Automating Expected Cost Analysis with Types
Di Wang,
David M. Kahn,
and Jan Hoffmann
In 25th International Conference on Functional Programming (ICFP’20).
2020
[pdf]
-
Exponential Automatic Amortized Resource Analysis
David Kahn,
and Jan Hoffmann
In 23rd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS’20).
2020
[pdf]
2019
-
BLT: Exact Bayesian Inference with Distribution Transformers
Charles Yuan,
and Jan Hoffmann
Technical Report.
2019
[pdf]
-
Resource-Guided Program Synthesis
Tristan Knoth,
Di Wang,
Jan Hoffmann,
and Nadia Polikarpova
In 40th Conference on Programming Language Design and Implementation (PLDI’19).
2019
[pdf]
[tr]
-
Type-Guided Worst-Case Input Generation
Di Wang,
and Jan Hoffmann
In 46th Symposium on Principles of Programming Languages (POPL’19).
2019
[pdf]
[slides]
[tr]
-
A Denotational Semantics for Low-Level Probabilistic Programs with Nondeterminism
Di Wang,
Jan Hoffmann,
and Thomas Reps
In Mathematical Foundations of Programming Semantics XXXV (MFPS’19).
2019
[pdf]
[slides]
[tr]
2018
-
Automatic Space Bound Analysis for Functional Programs with Garbage Collection
Yue Niu,
and Jan Hoffmann
In 22nd International Conference on Logic for
Programming Artificial Intelligence and Reasoning (LPAR’18).
2018
[pdf]
-
Parallel Complexity Analysis with Temporal Session Types
Ankush Das,
Jan Hoffmann,
and Frank Pfenning
In 23rd International Conference on Functional Programming (ICFP’18).
2018
[pdf]
-
Work Analysis with Resource-Aware Session Types
Ankush Das,
Jan Hoffmann,
and Frank Pfenning
In 33th ACM/IEEE Symposium on Logic in Computer Science (LICS’18).
2018
[pdf]
-
PMAF: An Algebraic Framework for Static Analysis of Probabilistic Programs
Di Wang,
Jan Hoffmann,
and Thomas Reps
In 39th Conference on Programming Language Design and Implementation (PLDI’18).
2018
[pdf]
[slides]
-
Bounded Expectations: Resource Analysis for Probabilistic Programs
Van Chan Ngo,
Quentin Carbonneaux,
and Jan Hoffmann
In 39th Conference on Programming Language Design and Implementation (PLDI’18).
2018
[pdf]
[tr]
[code]
2017
-
Arrays and References in Resource Aware ML
Benjamin Lichtman,
and Jan Hoffmann
In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD’17).
2017
[pdf]
-
-
ML for ML: Learning Cost Semantics by Experiment
Ankush Das,
and Jan Hoffmann
In 23rd International Conference on Tools and Algorithms
for the Construction and Analysis of Systems
(TACAS’17).
2017
[pdf]
-
Verifying and Synthesizing Constant-Resource Implementations
with Types
Van Chan Ngo,
Mario Dehesa-Azuara,
Matthew Fredrikson,
and Jan Hoffmann
In 38th IEEE Symposium on Security and Privacy (S&P ’17).
2017
[pdf]
[tr]
[code]
-
Relational Cost Analysis
Ezgi Çiçek,
Gilles Barthe,
Marco Gaboardi,
Deepak Garg,
and Jan Hoffmann
In 44th Symposium on Principles of Programming Languages (POPL’17).
2017
[pdf]
[tr]
-
Towards Automatic Resource Bound Analysis for OCaml
Jan Hoffmann,
Ankush Das,
and Shu-Chun Weng
In 44th Symposium on Principles of Programming Languages (POPL’17).
2017
[pdf]
[tr]
2016
-
Learning Cost Semantics for Modeling Running Time of OCaml Programs
Ankush Das,
and Jan Hoffmann
Presented at Syntax and Semantics of Low-Level Languages (LOLA’16).
2016
[pdf]
2015
-
Type-Based Amortized Resource Analysis with Integers and Arrays
Jan Hoffmann,
and Zhong Shao
J. Funct. Program..
2015
[pdf]
-
Compositional Certified Resource Bounds
Quentin Carbonneaux,
Jan Hoffmann,
and Zhong Shao
In 36th Conference on Programming Language Design and Implementation (PLDI’15).
Artifact submitted and approved.
2015
[pdf]
[tr]
-
Automatic Static Cost Analysis for Parallel Programs
Jan Hoffmann,
and Zhong Shao
In 24th European Symposium on Programming (ESOP’15).
2015
[pdf]
2014
-
Type-Based Amortized Resource Analysis with Integers and Arrays
Jan Hoffmann,
and Zhong Shao
In 12th International Symposium on Functional and Logic Programming (FLOPS’14).
2014
[pdf]
[tr]
-
End-to-End Verification of Stack-Space Bounds for C Programs
Quentin Carbonneaux,
Jan Hoffmann,
Tahina Ramananandro,
and Zhong Shao
In 35th Conference on Programming Language Design and Implementation (PLDI’14).
Artifact submitted and approved.
2014
[pdf]
[tr]
2013
-
Tracking Data-Flow with Open Closure Types
Gabriel Scherer,
and Jan Hoffmann
In 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR’13).
2013
[pdf]
-
Characterizing Progress Properties of Concurrent Objects via Contextual Refinements
Hongjin Liang,
Jan Hoffmann,
Xinyu Feng,
and Zhong Shao
In 24th International Conference on Concurrency Theory (CONCUR’13).
2013
[pdf]
[tr]
-
Quantitative Reasoning for Proving Lock-Freedom
Jan Hoffmann,
Michael Marmar,
and Zhong Shao
In 28th ACM/IEEE Symposium on Logic in Computer Science (LICS’13).
2013
[pdf]
[slides]
[tr]
-
The Complexity of Computing Minimal Unidirectional Covering
Sets
Dorothea Baumeister,
Felix Brandt,
Felix A. Fischer,
Jan Hoffmann,
and Jörg Rothe
Theory of Computing Systems.
2013
[pdf]
2012
-
Resource Aware ML
Jan Hoffmann,
Klaus Aehlig,
and Martin Hofmann
In 24rd International Conference on Computer Aided
Verification (CAV’12).
2012
[pdf]
-
Multivariate Amortized Resource Analysis
Jan Hoffmann,
Klaus Aehlig,
and Martin Hofmann
ACM Trans. Program. Lang. Syst..
2012
[pdf]
-
Higher-Order Functional Reactive Programming in Bounded Space
Neelakantan R. Krishnaswami,
Nick Benton,
and Jan Hoffmann
In 39th Symposium on Principles of Programming Languages (POPL’12).
2012
[pdf]
2011
-
Types with Potential: Polynomial Resource Bounds via Automatic Amortized Analysis
Jan Hoffmann
PhD Thesis.
Ludwig-Maximilians-Universität München.
2011
[pdf]
-
Multivariate Amortized Resource Analysis
Jan Hoffmann,
Klaus Aehlig,
and Martin Hofmann
In 38th Symposium on Principles of Programming Languages (POPL’11).
2011
[pdf]
2010
-
Amortized Resource Analysis with Polymorphic Recursion
and Partial Big-Step Operational Semantics
Jan Hoffmann,
and Martin Hofmann
In 8th Asian Symposium on Programming Languages (APLAS’10).
2010
[pdf]
[tr]
-
Amortized Resource Analysis with Polynomial Potential
Jan Hoffmann,
and Martin Hofmann
In 19th European Symposium on Programming (ESOP’10).
2010
[pdf]
[tr]
-
The Complexity of Computing Minimal Unidirectional Covering
Sets
Dorothea Baumeister,
Felix Brandt,
Felix A. Fischer,
Jan Hoffmann,
and Jörg Rothe
In Algorithms and Complexity, 7th International Conference (CIAC’10).
2010
[pdf]
-
2009
-
-
The Computational Complexity of Weak Saddles
Felix Brandt,
Markus Brill,
Felix A. Fischer,
and Jan Hoffmann
In Algorithmic Game Theory, Second International Symposium (SAGT’09).
2009
[pdf]
-
Finding a Tree Structure in a Resolution Proof is NP-Complete
Jan Hoffmann
Theoretical Computer Science.
2009
[pdf]
2008
-
Resolution Trees with Lemmas: Resolution Refinements that
Characterize DLL Algorithms with Clause Learning
Samuel R. Buss,
Jan Hoffmann,
and Jan Johannsen
Logical Methods in Computer Science.
2008
[pdf]
-
The NP-hardness of Finding a Directed Acyclic Graph for
Regular Resolution
Samuel R. Buss,
and Jan Hoffmann
Theoretical Computer Science.
2008
[pdf]
2007
-
Resolution Proofs and DLL-Algorithms with Clause Learning
Jan Hoffmann
Diploma Thesis, LMU München.
2007
[pdf]