Jules Jacobs
where else to find them
no profile links on file
what they talk about
all 4 in the filters
where they keep going back
- POPL4 editions2021–2024
- PLDI Workshop Honoring Andreas Podelski2 editions2024–2025
- ICFP2 editions2022–2023
all 4 in the filters
on a stage with
all 17 in the filters
who talks about the same things
- Jonas Kastberg Hinrichsen6 talks
- Stephanie Balzer10 talks
- Robbert Krebbers26 talks
- Amin Timany16 talks
- Lars Birkedal35 talks
- Jeehoon Kang14 talks
| title | conference | date |
|---|---|---|
| StacKAT: Infinite State Network Verification | PLDI 2025 | 2025-06-16 |
Defines StacKAT, a packet-language that adds a single variable-size stack payload with push/pop to NetKAT-style programs and proves program equivalence… | ||
| A Semantic Logical Relation for Termination of Intuitionistic Linear Logic Session Types | CoqPL 2025 | 2025-01-25 |
Proves termination for intuitionistic linear logic session types (ILLST) by building a semantic unary logical relation and showing the fundamental theorem… | ||
| KATch: A Fast Symbolic Verifier for NetKAT | PLDI 2024 | 2024-06-24 |
KATch implements NetKAT verification in Scala and replaces exhaustive packet enumeration with symbolic packets, BDD-style relations called SPs that are… | ||
| Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-O... | POPL 2024 | 2024-01-14 |
LinearActris is a linear concurrent separation logic that claims to give deadlock and leak freedom for message-passing programs by design. The adequacy proof… | ||
| Dependent Session Protocols in Separation Logic from First Principles | ICFP 2023 | 2023-09-04 |
Three-layer design builds session protocols from mutable references: one-shot channels, then functional session channels, then imperative endpoints; specs use… | ||
| Higher-Order Leak and Deadlock Free Locks | POPL 2023 | 2023-01-15 |
Presents a linearly typed lambda calculus that enforces both deadlock and memory-leak freedom for first-class, nestable locks, proving that well-typed programs… | ||
| Fast Coalgebraic Bisimilarity Minimization | POPL 2023 | 2023-01-15 |
Minimizes coalgebras (DFAs, transition systems, probabilistic/weighted automata) by repeatedly refining states via computed signatures and reusing unchanged… | ||
| Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Fre... | ICFP 2022 | 2022-09-11 |
A functional language MPGV extends GV with multiparty session types, first-class channel endpoints, dynamic spawning and a new redirect construct that enables… | ||
| Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation L | POPL 2022 | 2022-01-16 |
Introduces connectivity graphs as a generic, parametric graph abstraction plus local Separation Logic predicates that let one prove preservation and global… | ||
| Paradoxes of probabilistic programming | POPL 2021 | 2021-01-17 |
Probabilistic programs that multiply weights by pdfs produce unit errors and paradoxes: a simple height example gives 1.75 normally but a coin-conditional… | ||
| nothing matches | ||