default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDJan Hoffmann 0002
Person information
- affiliation: Carnegie Mellon University, Pittsburgh, PA, USA
- affiliation (former): Yale University, New Have, CT, USA
- affiliation (former): Ludwig-Maximilians-Universität München, Germany
Other persons with the same name
- Jan Hoffmann — disambiguation page
- Jan Hoffmann 0001 — Humboldt-Universität, Berlin, Germany
- Jan Hoffmann 0003 — Finisar, Berlin, Germany
- Jan Hoffmann 0004 — University of Stuttgart, Germany
- Jan Hoffmann 0005
![[0000-0001-9501-0874]](https://dblp.dagstuhl.de/img/orcid-mark.12x12.png "0000-0001-9501-0874")
— Braunschweig University of Technology, Institute for Electrical Machines, Traction and Drives, Germany
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
Books and Theses
- 2011
[b1]Jan Hoffmann:
Types with potential: polynomial resource bounds via automatic amortized analysis. Ludwig Maximilians University Munich, 2011, ISBN 978-3-8442-1516-8, pp. 1-179
Journal Articles
- 2024
- [j24]Long Pham, Jan Hoffmann:
Worst-Case Input Generation for Concurrent Programs under Non-Monotone Resource Metrics. Log. Methods Comput. Sci. 20(4) (2024) - [j23]Long Pham, Di Wang, Feras A. Saad, Jan Hoffmann:
Programmable MCMC with Soundly Composed Guide Programs. Proc. ACM Program. Lang. 8(OOPSLA2): 1051-1080 (2024) - [j22]Long Pham, Feras A. Saad, Jan Hoffmann:
Robust Resource Bounds with Static Analysis and Bayesian Inference. Proc. ACM Program. Lang. 8(PLDI): 76-101 (2024) - [j21]Stefan K. Muller, Jan Hoffmann:
Modeling and Analyzing Evaluation Cost of CUDA Kernels. ACM Trans. Parallel Comput. 11(1): 5:1-5:53 (2024) - 2023
- [j20]Ankush Das, Di Wang, Jan Hoffmann:
Probabilistic Resource-Aware Session Types. Proc. ACM Program. Lang. 7(POPL): 1925-1956 (2023) - 2022
- [j19]Jan Hoffmann, Donald Sannella, Ulrich Schöpp:
Preface for the special issue in homage to Martin Hofmann Part 2. Math. Struct. Comput. Sci. 32(6): 682-684 (2022) - [j18]Jan Hoffmann, Steffen Jost:
Two decades of automatic amortized resource analysis. Math. Struct. Comput. Sci. 32(6): 729-759 (2022) - 2021
- [j17]Jan Hoffmann, Donald Sannella, Ulrich Schöpp:
Preface for the special issue in homage to Martin Hofmann Part 1. Math. Struct. Comput. Sci. 31(9): 950-952 (2021) - [j16]David M. Kahn, Jan Hoffmann:
Automatic amortized resource analysis with the Quantum physicist's method. Proc. ACM Program. Lang. 5(ICFP): 1-29 (2021) - [j15]Stefan K. Muller, Jan Hoffmann:
Modeling and analyzing evaluation cost of CUDA kernels. Proc. ACM Program. Lang. 5(POPL): 1-31 (2021) - [j14]Vineet Rajani, Marco Gaboardi, Deepak Garg, Jan Hoffmann:
A unifying type-theory for higher-order (amortized) cost analysis. Proc. ACM Program. Lang. 5(POPL): 1-28 (2021) - 2020
- [j13]Tristan Knoth, Di Wang, Adam Reynolds, Jan Hoffmann, Nadia Polikarpova:
Liquid resource types. Proc. ACM Program. Lang. 4(ICFP): 106:1-106:29 (2020) - [j12]Di Wang, David M. Kahn, Jan Hoffmann:
Raising expectations: automating expected cost analysis with types. Proc. ACM Program. Lang. 4(ICFP): 110:1-110:31 (2020) - 2019
- [j11]Di Wang, Jan Hoffmann:
Type-guided worst-case input generation. Proc. ACM Program. Lang. 3(POPL): 13:1-13:30 (2019) - 2018
- [j10]Ankush Das, Jan Hoffmann, Frank Pfenning:
Parallel complexity analysis with temporal session types. Proc. ACM Program. Lang. 2(ICFP): 91:1-91:30 (2018) - 2017
- [j9]Jürgen Giesl, Jan Hoffmann:
Preface: Special Issue on Automatic Resource Bound Analysis. J. Autom. Reason. 59(1): 1-2 (2017) - 2015
- [j8]Jan Hoffmann, Zhong Shao:
Type-based amortized resource analysis with integers and arrays. J. Funct. Program. 25 (2015) - 2013
- [j7]Dorothea Baumeister, Felix Brandt, Felix A. Fischer, Jan Hoffmann, Jörg Rothe:
The Complexity of Computing Minimal Unidirectional Covering Sets. Theory Comput. Syst. 53(3): 467-502 (2013) - 2012
- [j6]Jan Hoffmann, Klaus Aehlig, Martin Hofmann:
Multivariate amortized resource analysis. ACM Trans. Program. Lang. Syst. 34(3): 14:1-14:62 (2012) - 2011
- [j5]Felix Brandt, Markus Brill, Felix A. Fischer, Jan Hoffmann:
The Computational Complexity of Weak Saddles. Theory Comput. Syst. 49(1): 139-161 (2011) - 2009
- [j4]Felix Brandt, Markus Brill, Felix A. Fischer, Paul Harrenstein, Jan Hoffmann:
Computing Shapley's saddles. SIGecom Exch. 8(2): 3 (2009) - [j3]Jan Hoffmann:
Finding a tree structure in a resolution proof is NP-complete. Theor. Comput. Sci. 410(21-23): 2295-2300 (2009) - 2008
- [j2]Samuel R. Buss, Jan Hoffmann, Jan Johannsen:
Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning. Log. Methods Comput. Sci. 4(4) (2008) - [j1]Samuel R. Buss, Jan Hoffmann:
The NP-hardness of finding a directed acyclic graph for regular resolution. Theor. Comput. Sci. 396(1-3): 271-276 (2008)
Conference and Workshop Papers
- 2023
- [c33]Jessie Grosen, David M. Kahn, Jan Hoffmann:
Automatic Amortized Resource Analysis with Regular Recursive Types. LICS 2023: 1-14 - 2021
- [c32]Ankush Das, Stephanie Balzer, Jan Hoffmann, Frank Pfenning, Ishani Santurkar:
Resource-Aware Session Types for Digital Contracts. CSF 2021: 1-16 - [c31]Long Pham, Jan Hoffmann:
Typable Fragments of Polynomial Automatic Amortized Resource Analysis. CSL 2021: 34:1-34:19 - [c30]Di Wang, Jan Hoffmann, Thomas W. Reps:
Central moment analysis for cost accumulators in probabilistic programs. PLDI 2021: 559-573 - [c29]Di Wang, Jan Hoffmann, Thomas W. Reps:
Sound probabilistic inference via guide types. PLDI 2021: 788-803 - 2020
- [c28]David M. Kahn, Jan Hoffmann:
Exponential Automatic Amortized Resource Analysis. FoSSaCS 2020: 359-380 - 2019
- [c27]Tristan Knoth, Di Wang, Nadia Polikarpova, Jan Hoffmann:
Resource-guided program synthesis. PLDI 2019: 253-268 - [c26]Di Wang, Jan Hoffmann, Thomas W. Reps:
A Denotational Semantics for Low-Level Probabilistic Programs with Nondeterminism. MFPS 2019: 303-324 - 2018
- [c25]Ankush Das, Jan Hoffmann, Frank Pfenning:
Work Analysis with Resource-Aware Session Types. LICS 2018: 305-314 - [c24]Yue Niu, Jan Hoffmann:
Automatic Space Bound Analysis for Functional Programs with Garbage Collection. LPAR 2018: 543-563 - [c23]Van Chan Ngo, Quentin Carbonneaux, Jan Hoffmann:
Bounded expectations: resource analysis for probabilistic programs. PLDI 2018: 496-512 - [c22]Di Wang, Jan Hoffmann, Thomas W. Reps:
PMAF: an algebraic framework for static analysis of probabilistic programs. PLDI 2018: 513-528 - 2017
- [c21]Quentin Carbonneaux, Jan Hoffmann, Thomas W. Reps, Zhong Shao:
Automated Resource Analysis with Coq Proof Objects. CAV (2) 2017: 64-85 - [c20]Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Jan Hoffmann:
Relational cost analysis. POPL 2017: 316-329 - [c19]Jan Hoffmann, Ankush Das, Shu-Chun Weng:
Towards automatic resource bound analysis for OCaml. POPL 2017: 359-373 - [c18]Benjamin Lichtman, Jan Hoffmann:
Arrays and References in Resource Aware ML. FSCD 2017: 26:1-26:20 - [c17]Van Chan Ngo, Mario Dehesa-Azuara, Matthew Fredrikson, Jan Hoffmann:
Verifying and Synthesizing Constant-Resource Implementations with Types. IEEE Symposium on Security and Privacy 2017: 710-728 - [c16]Ankush Das, Jan Hoffmann:
ML for ML: Learning Cost Semantics by Experiment. TACAS (1) 2017: 190-207 - 2015
- [c15]Jan Hoffmann, Zhong Shao:
Automatic Static Cost Analysis for Parallel Programs. ESOP 2015: 132-157 - [c14]Quentin Carbonneaux, Jan Hoffmann, Zhong Shao:
Compositional certified resource bounds. PLDI 2015: 467-478 - 2014
- [c13]Jan Hoffmann, Zhong Shao:
Type-Based Amortized Resource Analysis with Integers and Arrays. FLOPS 2014: 152-168 - [c12]Quentin Carbonneaux, Jan Hoffmann, Tahina Ramananandro, Zhong Shao:
End-to-end verification of stack-space bounds for C programs. PLDI 2014: 270-281 - 2013
- [c11]Hongjin Liang, Jan Hoffmann, Xinyu Feng, Zhong Shao:
Characterizing Progress Properties of Concurrent Objects via Contextual Refinements. CONCUR 2013: 227-241 - [c10]Jan Hoffmann, Michael Marmar, Zhong Shao:
Quantitative Reasoning for Proving Lock-Freedom. LICS 2013: 124-133 - [c9]Gabriel Scherer, Jan Hoffmann:
Tracking Data-Flow with Open Closure Types. LPAR 2013: 710-726 - 2012
- [c8]Jan Hoffmann, Klaus Aehlig, Martin Hofmann:
Resource Aware ML. CAV 2012: 781-786 - [c7]Neelakantan R. Krishnaswami, Nick Benton, Jan Hoffmann:
Higher-order functional reactive programming in bounded space. POPL 2012: 45-58 - 2011
- [c6]Jan Hoffmann, Klaus Aehlig, Martin Hofmann:
Multivariate amortized resource analysis. POPL 2011: 357-370 - 2010
- [c5]Jan Hoffmann, Martin Hofmann:
Amortized Resource Analysis with Polymorphic Recursion and Partial Big-Step Operational Semantics. APLAS 2010: 172-187 - [c4]Dorothea Baumeister, Felix Brandt, Felix A. Fischer, Jan Hoffmann, Jörg Rothe:
The Complexity of Computing Minimal Unidirectional Covering Sets. CIAC 2010: 299-310 - [c3]Jan Hoffmann:
An Automatic Amortized Analysis of the Resource Consumption of Functional Programs. AlgoSyn 2010: 151 - [c2]Jan Hoffmann, Martin Hofmann:
Amortized Resource Analysis with Polynomial Potential. ESOP 2010: 287-306 - 2009
- [c1]Felix Brandt, Markus Brill, Felix A. Fischer, Jan Hoffmann:
The Computational Complexity of Weak Saddles. SAGT 2009: 238-249
Informal and Other Publications
- 2025
- [i22]David M. Kahn, Jan Hoffmann, Thomas Reps, Jessie Grosen:
Efficient Cost Bounds with Linear Maps. CoRR abs/2509.22982 (2025) - 2023
- [i21]Jessie Grosen, David M. Kahn, Jan Hoffmann:
Automatic Amortized Resource Analysis with Regular Recursive Types. CoRR abs/2304.13627 (2023) - [i20]Long Pham, Jan Hoffmann:
Worst-Case Input Generation for Concurrent Programs under Non-Monotone Resource Metrics. CoRR abs/2309.01261 (2023) - 2021
- [i19]Di Wang, Jan Hoffmann, Thomas W. Reps:
Expected-Cost Analysis for Probabilistic Programs and Semantics-Level Adaption of Optional Stopping Theorems. CoRR abs/2103.16105 (2021) - [i18]Di Wang, Jan Hoffmann, Thomas W. Reps:
Sound Probabilistic Inference via Guide Types. CoRR abs/2104.03598 (2021) - [i17]David M. Kahn, Jan Hoffmann:
Automatic Amortized Resource Analysis with the Quantum Physicist's Method. CoRR abs/2106.13936 (2021) - 2020
- [i16]Di Wang, Jan Hoffmann, Thomas W. Reps:
Tail Bound Analysis for Probabilistic Programs via Central Moments. CoRR abs/2001.10150 (2020) - [i15]David M. Kahn, Jan Hoffmann:
Exponential Amortized Resource Analysis. CoRR abs/2002.09519 (2020) - [i14]Di Wang, David M. Kahn, Jan Hoffmann:
Raising Expectations: Automating Expected Cost Analysis with Types. CoRR abs/2006.14010 (2020) - [i13]Tristan Knoth, Di Wang, Adam Reynolds, Jan Hoffmann, Nadia Polikarpova:
Liquid Resource Types. CoRR abs/2006.16233 (2020) - [i12]Long Pham, Jan Hoffmann:
Typable Fragments of Polynomial Automatic Amortized Resource Analysis. CoRR abs/2010.16353 (2020) - [i11]Ankush Das, Di Wang, Jan Hoffmann:
Probabilistic Resource-Aware Session Types. CoRR abs/2011.09037 (2020) - 2019
- [i10]Ankush Das, Stephanie Balzer, Jan Hoffmann, Frank Pfenning:
Resource-Aware Session Types for Digital Contracts. CoRR abs/1902.06056 (2019) - [i9]Tristan Knoth, Di Wang, Nadia Polikarpova, Jan Hoffmann:
Resource-Guided Program Synthesis. CoRR abs/1904.07415 (2019) - 2018
- [i8]Van Chan Ngo, Mario Dehesa-Azuara, Matthew Fredrikson, Jan Hoffmann:
Verifying and Synthesizing Constant-Resource Implementations with Types. CoRR abs/1801.01896 (2018) - [i7]Ankush Das, Jan Hoffmann, Frank Pfenning:
Parallel Complexity Analysis with Temporal Session Types. CoRR abs/1804.06013 (2018) - 2017
- [i6]Van Chan Ngo, Quentin Carbonneaux, Jan Hoffmann:
Bounded Expectations: Resource Analysis for Probabilistic Programs. CoRR abs/1711.08847 (2017) - [i5]Ankush Das, Jan Hoffmann, Frank Pfenning:
Work Analysis with Resource-Aware Session Types. CoRR abs/1712.08310 (2017) - [i4]Marco Gaboardi, Jan Hoffmann, Reinhard Wilhelm, Florian Zuleger:
Resource Bound Analysis (Dagstuhl Seminar 17291). Dagstuhl Reports 7(7): 72-87 (2017) - 2016
- [i3]Jan Hoffmann, Ankush Das, Shu-Chun Weng:
Towards Automatic Resource Bound Analysis for OCaml. CoRR abs/1611.00692 (2016) - 2013
- [i2]Gabriel Scherer, Jan Hoffmann:
Tracking Data-Flow with Open Closure Types. CoRR abs/1312.0018 (2013) - 2008
- [i1]Samuel R. Buss, Jan Hoffmann, Jan Johannsen:
Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning. CoRR abs/0811.1075 (2008)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2025-10-22 00:20 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
