Jeehoon Kang
where else to find them
github:jeehoonkang
what they talk about
all 7 in the filters
where they keep going back
- PLDI Workshop Honoring Andreas Podelski4 editions2023–2026
- OOPSLA3 editions2023–2025
- POPL3 editions2021–2022
on a stage with
all 38 in the filters
who talks about the same things
- Janggun Lee7 talks
- Jaehwang Jung5 talks
- Sunho Park4 talks
- Michael Sammler16 talks
- Jaewoo Kim3 talks
- Lennard Gäher7 talks
| title | conference | date |
|---|---|---|
| Revisiting Partial Tracing for Safe, Efficient, and Concurrent Garbage Collection in(…) | PLDI 2026 | 2026-06-15 |
Implements a library-quality concurrent GC for unmanaged languages that keeps precise reference-counted roots and traces the heap, using phase consensus and a… | ||
| Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness | OOPSLA 2025 | 2025-10-16 |
Lilo is a higher-order concurrent separation logic that adds a promise mechanism to reason about liveness: threads record a promise list and must consume… | ||
| Leveraging Immutability to Validate Hazard Pointers for Optimistic Traversals | PLDI 2025 | 2025-06-16 |
Presents a new hazard-pointer validation that exploits the immutability of marked nodes to validate reachability by checking the most recent unmarked… | ||
| Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic | PLDI 2025 | 2025-06-16 |
First formal verification of a general-purpose RCU under relaxed memory consistency, proving a modular spec that supports modular specification, switchable… | ||
| Verifying Lock-Free Traversals in Relaxed Memory Separation Logic | PLDI 2025 | 2025-06-16 |
First mechanized verification of a lock-free linked list, skiplist, and skiplist-based priority queue against relaxed memory consistency, using the iRC11… | ||
| Quantum Probabilistic Model Checking for Time-Bounded Properties | OOPSLA 2024 | 2024-10-20 |
Encodes time-bounded probabilistic model checking as quantum circuits that superpose the 2^n state distribution, implements state transition circuits by… | ||
| Modular Hardware Design of Pipelined Circuits with Hazards | PLDI 2024 | 2024-06-24 |
Proposes hazard interfaces that generalize valid-ready by carrying arbitrary “reserve” values and a ready function, plus map-reduce style combinators that… | ||
| Concurrent Immediate Reference Counting | PLDI 2024 | 2024-06-24 |
A new system, Concurrent Immediate Reference Counting, combines reference counting with SMR (EBR) to record a decrement EPO per object and use a global epoch… | ||
| A Proof Recipe for Linearizability in Relaxed Memory Separation Logic | PLDI 2024 | 2024-06-24 |
This work gives a concrete proof recipe and mechanization in Coq (Iris-based iRC11) that reduces manual effort by about 81% via automation, introduces object… | ||
| Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic | OOPSLA 2023 | 2023-10-23 |
Proposes modular, machine-checked specs for hazard pointers and RCU and proves realistic reclamation implementations in Coq, mechanized in Iris. Claims… | ||
| Memento: A Framework for Detectable Recoverability in Persistent Memory | PLDI 2023 | 2023-06-17 |
Memento is a programming framework that proves and enforces detectable recoverability for persistent memory by using a timestamp-based recovery strategy plus… | ||
| The Future of Concurrency and Parallelism | POPL 2022 Virtual Workshop | 2022-01-27 |
Panelists contrast concrete methods and hard surprises: mechanized proofs in Coq/Agda and concurrent separation logic are used to prove deadlock freedom and… | ||
| Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz | POPL 2022 | 2022-01-16 |
Framework claims a mechanically checked simulation that preserves contextual refinement and termination under a fair scheduler for real concurrent compiler… | ||
| Doing Research in PL panel | POPL 2021 | 2021-01-17 |
Recent concrete work reported includes a postdoc-built prototype that replaces P4’s hand‑rolled state‑machine parsers with a compositional parser design, a… | ||
| nothing matches | ||