Ike Mulder
where else to find them
what they talk about
where they keep going back
- PLDI Workshop Honoring Andreas Podelski2 editions2023–2024
on a stage with
- Robbert Krebbers4×
- Jaehwang Jungonce
- Jaewoo Kimonce
all 7 in the filters
who talks about the same things
- Janggun Lee7 talks
- Sunho Park4 talks
- Robbert Krebbers26 talks
- Jaehwang Jung5 talks
- Jaewoo Kim3 talks
- Jeehoon Kang14 talks
| title | conference | date |
|---|---|---|
| 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… | ||
| Unification for Subformula Linking under Quantifiers | CPP 2024 | 2024-01-15 |
Proposes Quantifying on the Uninstantiated, a unification-based algorithm that retroactively turns Evars found during matching into existential quantifiers, so… | ||
| Proof Automation for Linearizability in Separation Logic | OOPSLA 2023 | 2023-10-23 |
Implements proof automation for contextual refinement and logical atomicity inside Diaframe 2.0, encoded in Iris and Coq, and uses both program shape and… | ||
| Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic | PLDI 2023 | 2023-06-17 |
Proposes a connection-based multi-succedent calculus that reduces blind backtracking for disjunctive invariants in fine-grained concurrent separation logic… | ||
| nothing matches | ||