Jan Hoffmann

82 papers A* 16A 3B 9C 1Misc 1Journal 48Unranked 3
YearRankTypeTitle / Venue / Authors
2026 J jnl
Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment.
Proc. ACM Program. Lang.
David M. Kahn, Jan Hoffmann, Runming Li
2025 J jnl
Efficient Cost Bounds with Linear Maps.
CoRR
David M. Kahn, Jan Hoffmann, Thomas Reps, Jessie Grosen
2025 J jnl
Integrating Resource Analyses via Resource Decomposition.
Proc. ACM Program. Lang.
Long Pham, Yue Niu, Nathan Glover, Feras Saad, Jan Hoffmann
2024 J jnl
Modeling and Analyzing Evaluation Cost of CUDA Kernels.
ACM Trans. Parallel Comput.
Stefan K. Muller, Jan Hoffmann
2024 J jnl
Programmable MCMC with Soundly Composed Guide Programs.
Proc. ACM Program. Lang.
Long Pham, Di Wang, Feras A. Saad, Jan Hoffmann
2024 J jnl
Robust Resource Bounds with Static Analysis and Bayesian Inference.
Proc. ACM Program. Lang.
Long Pham, Feras A. Saad, Jan Hoffmann
2024 J jnl
Worst-Case Input Generation for Concurrent Programs under Non-Monotone Resource Metrics.
Log. Methods Comput. Sci.
Long Pham, Jan Hoffmann
2023 A* conf
Automatic Amortized Resource Analysis with Regular Recursive Types.
LICS
Jessie Grosen, David M. Kahn, Jan Hoffmann
2023 J jnl
Automatic Amortized Resource Analysis with Regular Recursive Types.
CoRR
Jessie Grosen, David M. Kahn, Jan Hoffmann
2023 J jnl
Probabilistic Resource-Aware Session Types.
Proc. ACM Program. Lang.
Ankush Das, Di Wang, Jan Hoffmann
2023 J jnl
Worst-Case Input Generation for Concurrent Programs under Non-Monotone Resource Metrics.
CoRR
Long Pham, Jan Hoffmann
2022 J jnl
Preface for the special issue in homage to Martin Hofmann Part 2.
Math. Struct. Comput. Sci.
Jan Hoffmann, Donald Sannella, Ulrich Schöpp
2022 J jnl
Two decades of automatic amortized resource analysis.
Math. Struct. Comput. Sci.
Jan Hoffmann, Steffen Jost
2021 J jnl
A unifying type-theory for higher-order (amortized) cost analysis.
Proc. ACM Program. Lang.
Vineet Rajani, Marco Gaboardi, Deepak Garg, Jan Hoffmann
2021 J jnl
Automatic Amortized Resource Analysis with the Quantum Physicist's Method.
CoRR
David M. Kahn, Jan Hoffmann
2021 J jnl
Automatic amortized resource analysis with the Quantum physicist's method.
Proc. ACM Program. Lang.
David M. Kahn, Jan Hoffmann
2021 A* conf
Central moment analysis for cost accumulators in probabilistic programs.
PLDI
Di Wang, Jan Hoffmann, Thomas W. Reps
2021 J jnl
Expected-Cost Analysis for Probabilistic Programs and Semantics-Level Adaption of Optional Stopping Theorems.
CoRR
Di Wang, Jan Hoffmann, Thomas W. Reps
2021 J jnl
Modeling and analyzing evaluation cost of CUDA kernels.
Proc. ACM Program. Lang.
Stefan K. Muller, Jan Hoffmann
2021 J jnl
Preface for the special issue in homage to Martin Hofmann Part 1.
Math. Struct. Comput. Sci.
Jan Hoffmann, Donald Sannella, Ulrich Schöpp
2021 A conf
Resource-Aware Session Types for Digital Contracts.
CSF
Ankush Das, Stephanie Balzer, Jan Hoffmann, Frank Pfenning, Ishani Santurkar
2021 J jnl
Sound Probabilistic Inference via Guide Types.
CoRR
Di Wang, Jan Hoffmann, Thomas W. Reps
2021 A* conf
Sound probabilistic inference via guide types.
PLDI
Di Wang, Jan Hoffmann, Thomas W. Reps
2021 B conf
Typable Fragments of Polynomial Automatic Amortized Resource Analysis.
CSL
Long Pham, Jan Hoffmann
2020 J jnl
Exponential Amortized Resource Analysis.
CoRR
David M. Kahn, Jan Hoffmann
2020 B conf
Exponential Automatic Amortized Resource Analysis.
FoSSaCS
David M. Kahn, Jan Hoffmann
2020 J jnl
Liquid Resource Types.
CoRR
Tristan Knoth, Di Wang, Adam Reynolds, Jan Hoffmann, Nadia Polikarpova
2020 J jnl
Liquid resource types.
Proc. ACM Program. Lang.
Tristan Knoth, Di Wang, Adam Reynolds, Jan Hoffmann, Nadia Polikarpova
2020 J jnl
Probabilistic Resource-Aware Session Types.
CoRR
Ankush Das, Di Wang, Jan Hoffmann
2020 J jnl
Raising Expectations: Automating Expected Cost Analysis with Types.
CoRR
Di Wang, David M. Kahn, Jan Hoffmann
2020 J jnl
Raising expectations: automating expected cost analysis with types.
Proc. ACM Program. Lang.
Di Wang, David M. Kahn, Jan Hoffmann
2020 J jnl
Tail Bound Analysis for Probabilistic Programs via Central Moments.
CoRR
Di Wang, Jan Hoffmann, Thomas W. Reps
2020 J jnl
Typable Fragments of Polynomial Automatic Amortized Resource Analysis.
CoRR
Long Pham, Jan Hoffmann
2019 B conf
A Denotational Semantics for Low-Level Probabilistic Programs with Nondeterminism.
MFPS
Di Wang, Jan Hoffmann, Thomas W. Reps
2019 J jnl
Resource-Aware Session Types for Digital Contracts.
CoRR
Ankush Das, Stephanie Balzer, Jan Hoffmann, Frank Pfenning
2019 J jnl
Resource-Guided Program Synthesis.
CoRR
Tristan Knoth, Di Wang, Nadia Polikarpova, Jan Hoffmann
2019 A* conf
Resource-guided program synthesis.
PLDI
Tristan Knoth, Di Wang, Nadia Polikarpova, Jan Hoffmann
2019 J jnl
Type-guided worst-case input generation.
Proc. ACM Program. Lang.
Di Wang, Jan Hoffmann
2018 B conf
Automatic Space Bound Analysis for Functional Programs with Garbage Collection.
LPAR
Yue Niu, Jan Hoffmann
2018 A* conf
Bounded expectations: resource analysis for probabilistic programs.
PLDI
Van Chan Ngo, Quentin Carbonneaux, Jan Hoffmann
2018 A* conf
PMAF: an algebraic framework for static analysis of probabilistic programs.
PLDI
Di Wang, Jan Hoffmann, Thomas W. Reps
2018 J jnl
Parallel Complexity Analysis with Temporal Session Types.
CoRR
Ankush Das, Jan Hoffmann, Frank Pfenning
2018 J jnl
Parallel complexity analysis with temporal session types.
Proc. ACM Program. Lang.
Ankush Das, Jan Hoffmann, Frank Pfenning
2018 J jnl
Verifying and Synthesizing Constant-Resource Implementations with Types.
CoRR
Van Chan Ngo, Mario Dehesa-Azuara, Matthew Fredrikson, Jan Hoffmann
2018 A* conf
Work Analysis with Resource-Aware Session Types.
LICS
Ankush Das, Jan Hoffmann, Frank Pfenning
2017 B conf
Arrays and References in Resource Aware ML.
FSCD
Benjamin Lichtman, Jan Hoffmann
2017 — conf
Automated Resource Analysis with Coq Proof Objects.
CAV (2)
Quentin Carbonneaux, Jan Hoffmann, Thomas W. Reps, Zhong Shao
2017 J jnl
Bounded Expectations: Resource Analysis for Probabilistic Programs.
CoRR
Van Chan Ngo, Quentin Carbonneaux, Jan Hoffmann
2017 — conf
ML for ML: Learning Cost Semantics by Experiment.
TACAS (1)
Ankush Das, Jan Hoffmann
2017 J jnl
Preface: Special Issue on Automatic Resource Bound Analysis.
J. Autom. Reason.
Jürgen Giesl, Jan Hoffmann
2017 A* conf
Relational cost analysis.
POPL
Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Jan Hoffmann
2017 J jnl
Resource Bound Analysis (Dagstuhl Seminar 17291).
Dagstuhl Reports
Marco Gaboardi, Jan Hoffmann, Reinhard Wilhelm, Florian Zuleger
2017 A* conf
Towards automatic resource bound analysis for OCaml.
POPL
Jan Hoffmann, Ankush Das, Shu-Chun Weng
2017 A* conf
Verifying and Synthesizing Constant-Resource Implementations with Types.
IEEE Symposium on Security and Privacy
Van Chan Ngo, Mario Dehesa-Azuara, Matthew Fredrikson, Jan Hoffmann
2017 J jnl
Work Analysis with Resource-Aware Session Types.
CoRR
Ankush Das, Jan Hoffmann, Frank Pfenning
2016 J jnl
Towards Automatic Resource Bound Analysis for OCaml.
CoRR
Jan Hoffmann, Ankush Das, Shu-Chun Weng
2015 A conf
Automatic Static Cost Analysis for Parallel Programs.
ESOP
Jan Hoffmann, Zhong Shao
2015 A* conf
Compositional certified resource bounds.
PLDI
Quentin Carbonneaux, Jan Hoffmann, Zhong Shao
2015 J jnl
Type-based amortized resource analysis with integers and arrays.
J. Funct. Program.
Jan Hoffmann, Zhong Shao
2014 A* conf
End-to-end verification of stack-space bounds for C programs.
PLDI
Quentin Carbonneaux, Jan Hoffmann, Tahina Ramananandro, Zhong Shao
2014 Misc conf
Type-Based Amortized Resource Analysis with Integers and Arrays.
FLOPS
Jan Hoffmann, Zhong Shao
2013 B conf
Characterizing Progress Properties of Concurrent Objects via Contextual Refinements.
CONCUR
Hongjin Liang, Jan Hoffmann, Xinyu Feng, Zhong Shao
2013 A* conf
Quantitative Reasoning for Proving Lock-Freedom.
LICS
Jan Hoffmann, Michael Marmar, Zhong Shao
2013 J jnl
The Complexity of Computing Minimal Unidirectional Covering Sets.
Theory Comput. Syst.
Dorothea Baumeister, Felix Brandt, Felix A. Fischer, Jan Hoffmann, Jörg Rothe
2013 B conf
Tracking Data-Flow with Open Closure Types.
LPAR
Gabriel Scherer, Jan Hoffmann
2013 J jnl
Tracking Data-Flow with Open Closure Types.
CoRR
Gabriel Scherer, Jan Hoffmann
2012 A* conf
Higher-order functional reactive programming in bounded space.
POPL
Neelakantan R. Krishnaswami, Nick Benton, Jan Hoffmann
2012 J jnl
Multivariate amortized resource analysis.
ACM Trans. Program. Lang. Syst.
Jan Hoffmann, Klaus Aehlig, Martin Hofmann
2012 A* conf
Resource Aware ML.
CAV
Jan Hoffmann, Klaus Aehlig, Martin Hofmann
2011 A* conf
Multivariate amortized resource analysis.
POPL
Jan Hoffmann, Klaus Aehlig, Martin Hofmann
2011 J jnl
The Computational Complexity of Weak Saddles.
Theory Comput. Syst.
Felix Brandt, Markus Brill, Felix A. Fischer, Jan Hoffmann
2011 — —
Types with potential: polynomial resource bounds via automatic amortized analysis.
Jan Hoffmann
2010 B conf
Amortized Resource Analysis with Polymorphic Recursion and Partial Big-Step Operational Semantics.
APLAS
Jan Hoffmann, Martin Hofmann
2010 A conf
Amortized Resource Analysis with Polynomial Potential.
ESOP
Jan Hoffmann, Martin Hofmann
2010 — conf
An Automatic Amortized Analysis of the Resource Consumption of Functional Programs.
AlgoSyn
Jan Hoffmann
2010 C conf
The Complexity of Computing Minimal Unidirectional Covering Sets.
CIAC
Dorothea Baumeister, Felix Brandt, Felix A. Fischer, Jan Hoffmann, Jörg Rothe
2009 J jnl
Computing Shapley's saddles.
SIGecom Exch.
Felix Brandt, Markus Brill, Felix A. Fischer, Paul Harrenstein, Jan Hoffmann
2009 J jnl
Finding a tree structure in a resolution proof is NP-complete.
Theor. Comput. Sci.
Jan Hoffmann
2009 B conf
The Computational Complexity of Weak Saddles.
SAGT
Felix Brandt, Markus Brill, Felix A. Fischer, Jan Hoffmann
2008 J jnl
Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
CoRR
Samuel R. Buss, Jan Hoffmann, Jan Johannsen
2008 J jnl
Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning.
Log. Methods Comput. Sci.
Samuel R. Buss, Jan Hoffmann, Jan Johannsen
2008 J jnl
The NP-hardness of finding a directed acyclic graph for regular resolution.
Theor. Comput. Sci.
Samuel R. Buss, Jan Hoffmann