Joseph Tassarotti
where else to find them
what they talk about
all 5 in the filters
where they keep going back
- POPL4 editions2022–2026
- PLDI Workshop Honoring Andreas Podelski3 editions2023–2026
- ICFP2 editions2022–2025
all 8 in the filters
on a stage with
all 34 in the filters
who talks about the same things
- Alejandro Aguirre10 talks
- Kwing Hei Li6 talks
- Simon Oddershede Gregersen9 talks
- Philipp G. Haselwarter6 talks
- Lars Birkedal35 talks
- Amin Timany16 talks
| title | conference | date |
|---|---|---|
| Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation(…) | PLDI 2026 | 2026-06-15 |
Claims a program logic that encodes privacy budget as resource inside a probabilistic higher-order separation logic, proves an adequacy theorem linking the… | ||
| Contextual Refinement of Higher-Order Concurrent Probabilistic Programs | PLDI 2026 | 2026-06-15 |
Claims a new logic, Foxtrot, that proves contextual refinement for higher-order concurrent probabilistic programs and handles higher-order local state… | ||
| Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and(…) | POPL 2026 | 2026-01-11 |
Introduces Probabilistic Concurrent Outcome Logic (pcOL) that composes concurrent separation logic, probabilistic separation logic, and Outcome Logic to prove… | ||
| All for One and One for All: Program Logics for Exploiting Internal Determinism in(…) | POPL 2026 | 2026-01-11 |
Defines schedule-independent safety: showing one terminating execution is safe suffices to guarantee safety for all schedules. Introduces separation logic… | ||
| Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs | ICFP 2025 | 2025-10-12 |
Presents Coneris, the first higher-order concurrent separation logic that proves numeric error bounds for concurrent probabilistic programs and mechanizes all… | ||
| Verified Foundations for Differential Privacy | PLDI 2025 | 2025-06-16 |
SampCert is a mechanized foundation for differential privacy written in Lean that proves correctness of sampling and DP composition and ships verified samplers… | ||
| Approximate Relational Reasoning for Higher-Order Probabilistic Programs | POPL 2025 | 2025-01-19 |
Describes Approxis, a higher-order separation logic that treats error credits as first-class resources to prove approximate program refinements for an ML-like… | ||
| A Demonic Outcome Logic for Randomized Nondeterminism | POPL 2025 | 2025-01-19 |
Introduces Demonic Outcome Logic that models randomized programs with adversarial nondeterminism using the convex power set semantics, proving a distributive… | ||
| Tachis: Higher-Order Separation Logic with Credits for Expected Costs | OOPSLA 2024 | 2024-10-20 |
Tachis introduces probabilistic cost credits, a separation logic resource that preserves expectation across random branches and lets proofs allocate credits… | ||
| Day opening | Dafny 2024 | 2024-01-14 |
This session delivers logistics and a roadmap not technical results: 18 talks across five sessions, running 9:00–6:00 with 15+3 minute slots, plus Q&A and… | ||
| Asynchronous Probabilistic Couplings in Higher-Order Separation Logic | POPL 2024 | 2024-01-14 |
Provides a new higher-order relational separation logic called Clutch that proves contextual refinement for a language with impredicative polymorphism… | ||
| Day closing | Dafny 2024 | 2024-01-14 |
Day closing gives practical logistics and requests: organizers ask for written feedback for future conferences and topics, note a planned meetup at 6:45 at the… | ||
| Verifying vMVCC, a high-performance transaction library using multi-version concurrency.. | OSDI 2023 | 2023-07-10 |
vMVCC claims to be the first MVCC transaction library with a machine-checked proof and ships as about 800 lines of Go (open source). It implements in-memory… | ||
| Leakage models are a leaky abstraction (...) | PLARCH 2023 | 2023-06-17 |
They verify timing by symbolically executing gate‑level RTL instead of assuming leakage models, translating circuits to Rosette and running a symbolic RTL… | ||
| Verified Density Compilation for a Probabilistic Programming Language | PLDI 2023 | 2023-06-17 |
Provides a mechanized semantics for a Stan subset and verifies three density-compilation passes in Coq, producing ProbCompCert that connects to CompCert down… | ||
| Later Credits: Resourceful Reasoning for the Later Modality | ICFP 2022 | 2022-09-11 |
Introduces later credits as an ownable resource in Iris that splits stepping into a credit-generation rule and a credit-spending rule, letting proofs prepay… | ||
| A Separation Logic for Negative Dependence | POPL 2022 | 2022-01-16 |
Design of LINA, a probabilistic separation logic that adds a second separating conjunction for negative dependence alongside the independence star, with… | ||
| GoJournal: a verified, concurrent, crash-safe journaling system | 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI '21) | 2021-07-14 |
GoJournal implements a verified, concurrent, crash-safe journaling API in Go and proves it in Coq with Perennial 2.0, using the Goose translator to model Go… | ||
| nothing matches | ||