Alejandro Aguirre
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–2025
all 5 in the filters
on a stage with
all 16 in the filters
who talks about the same things
- Kwing Hei Li6 talks
- Simon Oddershede Gregersen9 talks
- Philipp G. Haselwarter6 talks
- Joseph Tassarotti20 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… | ||
| Modular Specifications and Implementations of Random Samplers in Higher-Order Separation(…) | CPP 2026 | 2026-01-12 |
Defines a reusable distribution typeclass for Eris (Iris-based) that internalizes sampler reasoning, proves a distribution adequacy theorem linking the logical… | ||
| 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… | ||
| 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… | ||
| Modelling Recursion and Probabilistic Choice in Guarded Type Theory | POPL 2025 | 2025-01-19 |
Paper encodes FPC⊕ (recursive types + probabilistic choice) inside clocked guarded type theory and builds operational and denotational semantics connected by a… | ||
| 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… | ||
| 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… | ||
| Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Ch... | POPL 2023 | 2023-01-15 |
Paper defines operational notions of may- and must-termination as optimal and pessimal termination probabilities, and builds step-indexed logical relations… | ||
| A Pre-Expectation Calculus for Probabilistic Sensitivity | POPL 2021 | 2021-01-17 |
A relational pre-expectation calculus gives computable upper bounds on the Kantorovich lifting of output distributions, proved sound and (in cases) continuous… | ||
| nothing matches | ||