Peter Thiemann
where else to find them
no profile links on file
what they talk about
all 8 in the filters
where they keep going back
all 11 in the filters
on a stage with
all 10 in the filters
who talks about the same things
- Hannes Saffrich4 talks
- Janek Spaderna3 talks
- Brigitte Pientka15 talks
- Jan Hoffmann9 talks
- Deepak Garg18 talks
- Ankush Das6 talks
| title | conference | date |
|---|---|---|
| Wasmgrind: Towards Dynamic Concurrency Analysis for Multithreaded WebAssembly | WebAssembly Workshop @ ICFP/SPLASH 2025 | 2025-10-16 |
Wasmgrind implements an instrumentation framework that generates offline traces for race and deadlock prediction, proving an embedder-agnostic ABI that exposes… | ||
| Borrowing From Session Types | OOPSLA 2025 | 2025-10-16 |
Proposes BGV, a session‑type API that replaces resource‑passing with borrowing via a split primitive that carves a channel into a single‑action borrow and a… | ||
| Ordered Types for Typestate | IWACO 2024 | 2024-10-21 |
Derives a calculus that encodes typestate as sets of allowed future traces and uses ordered context semicolons as temporal consumption order, so borrows are… | ||
| A silent semantics for isorecursive session types | ST30 2023 | 2023-10-22 |
Claim: isorecursive session types can often avoid runtime roll/unroll if all recursions are contractive isorecursive types, and an algorithm extracts adapter… | ||
| Polymorphic Typestate for Session Types | PPDP 2023 | 2023-10-22 |
Claims that a typestate-based model, using PolyVGR with higher-order polymorphism and existential types, matches the expressivity of functional and linear… | ||
| Towards Tagless Interpretation of Stratified System F (Extended Abstract) | TyDe 2023 | 2023-09-04 |
An intrinsically typed, tagless interpreter for a stratified fragment of System F is formalized in Agda: types carry natural-number levels and map to Set_l so… | ||
| Intrinsically Typed Sessions with Callbacks | ICFP 2023 | 2023-09-04 |
Claims a practical embedding of session types that avoids host-language linear types by representing protocols as an indexed command data structure of… | ||
| Parameterized Algebraic Protocols | PLDI 2023 | 2023-06-17 |
The work defines algebraic session types that name recursion like algebraic datatypes and claim type equivalence becomes linear-time nominal check instead of… | ||
| Session Types Meet Polymorphism and Dependent Types | PLMW @ POPL 2023 | 2023-01-17 |
[PLMW @ POPL'23] Session Types Meet Polymorphism and Dependent Types
Peter Thiemann
We live in a world of connected services where geographically separate… | ||
| Kindly Bent to Free Us | SPLASH 2022 | 2022-12-05 |
Affe is an ML extension that enforces single-use and drop-able resources by inferring linear and affine kinds and lexical regions and solving constrained-kind… | ||
| Label dependent lambda calculus and gradual typing | SPLASH 2022 | 2022-12-05 |
Defines a minimalist label-dependent lambda calculus with first-class labels, Pi/Sigma/singleton types and subtyping, then gives a gradual extension with a… | ||
| A Typed Programmatic Interface to Contracts on the Blockchain | APLAS 2021 | 2021-10-17 |
Defines a concrete, type-safe interaction between OCaml programs and Tezos contracts and proves preservation and progress for that execution model. Provides a… | ||
| Label Dependent Lambda Calculus and Gradual Typing | OOPSLA 2021 | 2021-10-17 |
A small dependently typed core called the label-dependent lambda calculus models records as functions over first-class labels and adds lightweight… | ||
| Kindly Bent to Free Us | ICFP 2020 | 2020-08-23 |
A new ML extension called Affe enforces linearity and affinity so a database use-after-free example compiles in OCaml but is rejected at compile time here. It… | ||
| nothing matches | ||