Jan Hoffmann
where else to find them
no profile links on file
what they talk about
where they keep going back
- POPL3 editions2021–2026
all 5 in the filters
on a stage with
all 13 in the filters
who talks about the same things
- Di Wang12 talks
- Deepak Garg18 talks
- Joost-Pieter Katoen14 talks
- Long Pham2 talks
- Gilles Barthe17 talks
- Mathieu Huot11 talks
| title | conference | date |
|---|---|---|
| Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment | POPL 2026 | 2026-01-11 |
Extends big-step semantics with a nondeterministic big-stop rule schema that captures every finite prefix of diverging small-step runs, proving equivalence to… | ||
| Programmable MCMC with Soundly Composed Guide Programs | OOPSLA 2024 | 2024-10-20 |
Implements a coroutine-based framework and a type system that encodes the message protocol between a model program and a sequence of block-wise guide programs… | ||
| Robust Resource Bounds with Static Analysis and Bayesian Inference | PLDI 2024 | 2024-06-24 |
Claims a combined static/data technique that actually implements and evaluates a hybrid: it integrates automatic amortized resource analysis (AARA) with… | ||
| Probabilistic Resource-Aware Session Types | POPL 2023 | 2023-01-15 |
Extends binary session types to describe message probability distributions and to infer expected-resource bounds automatically, using a type reconstruction… | ||
| A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis | POPL 2021 | 2021-01-17 |
Presents λ-amor, an affine type theory that adds a modal potential type plus a graded cost monad and refinements, and proves soundness with a Kripke… | ||
| Modeling and Analyzing Evaluation Cost of CUDA Kernels | POPL 2021 | 2021-01-17 |
Paper presents a quantitative program logic and cost semantics for CUDA that are formalized in Coq formalization and implemented as the prototype tool vercuta… | ||
| Liquid Resource Types | ICFP 2020 | 2020-08-23 |
Liquid Resource Types claims an automated refinement-type system that proves precise, value-dependent resource bounds (polynomial, exponential and fine-grained… | ||
| Raising Expectations: Automating Expected Cost Analysis with Types | ICFP 2020 | 2020-08-23 |
A type-based tool called PRaML automatically infers upper bounds on expected execution cost for probabilistic OCaml-like programs by extending RaML’s AARA… | ||
| Automatic Resource Bound Analysis and Linear Optimization | Learning, Algorithm Design and Beyond Worst-Case Analysis | 2016-11-14 |
Automatic system generates symbolic worst‑case resource bounds by encoding type‑based potential annotations into linear constraints and solving them with LP… | ||
| nothing matches | ||