Marco Gaboardi
where else to find them
what they talk about
all 7 in the filters
where they keep going back
- POPL3 editions2021–2026
- PLDI Workshop Honoring Andreas Podelski3 editions2024–2026
all 10 in the filters
on a stage with
all 22 in the filters
who talks about the same things
- Deepak Garg18 talks
- Amal Ahmed25 talks
- Gilles Barthe17 talks
- Lars Birkedal35 talks
- Joseph Tassarotti20 talks
- Steve Zdancewic19 talks
| title | conference | date |
|---|---|---|
| Practical Extensions for Graded Monads | HOPE 2026 | 2026-08-24 |
Extends graded monads by indexing grades with typed Kleene algebra (regular-language-style operations) and gives an operational semantics via the free monad… | ||
| Relational Cell Morphing: Automated Verification of Relational Properties of Array(…) | ARRAY 2026 | 2026-06-16 |
The system reduces relational verification of array programs to constrained Horn clause solving over scalars by tracking a few distinguished cells across two… | ||
| Probabilistic Refinement Session Types | PLDI 2026 | 2026-06-15 |
Introduces probabilistic refinement session types and implements a prototype PReST prototype in OCaml with a bi-directional type checker that emits nonlinear… | ||
| Cryptis: Cryptographic Reasoning in Separation Logic | POPL 2026 | 2026-01-11 |
Cryptis extends Iris separation logic with a symbolic-cryptography model and gives protocol specs that actually exchange separation-logic resources so proofs… | ||
| Probabilistic Refinement Session Types | PLDI 2025 | 2025-06-16 |
Introduces PReST, a core calculus that generalizes probabilistic session types to symbolic probabilities and proves type safety, global progress, probability… | ||
| Domain Reasoning In TopKAT: Reduction and Completeness | TPSA 2025 | 2025-01-19 |
TopKAT is incomplete over relational models: there exists an inequality true in every relational TopKAT but unprovable from TopKAT axioms, yet adding that… | ||
| Sensitivity by Parametricity | OOPSLA 2024 | 2024-10-20 |
A method reduces proving a function’s sensitivity to ordinary type-checking by encoding metric relations at the type level and exploiting parametric… | ||
| Program Analysis for Adaptive Data Analysis | PLDI 2024 | 2024-06-24 |
Static analysis estimates the adaptivity of while-like adaptive data analyses by building a weighted dependency graph whose node weights are reachability upper… | ||
| ICFP 2024 announcement | ICFP 2023 | 2023-09-04 |
ICFP 2024 will be in Milan, Italy, with the main venue a conference center (not a hotel) offering a full-floor program space and basement rooms for workshops… | ||
| Verified Differential Privacy for Finite Computers | CoqPL 2023 | 2023-01-21 |
Coq formalization implements the Geometric Truncated Mechanism using Coq with finprob and rat and proves both an approximate bound (Alpha Prime) and when… | ||
| 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… | ||
| On Incorrectness Logic and Kleene Algebra with Top and Tests | POPL 2022 | 2022-01-16 |
Kleene Algebra with Tests (KAT) cannot express incorrectness triples because it lacks an explicit codomain operation; adding a single top element yields… | ||
| A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis | POPL 2021 | 2021-01-17 |
Presents λ-amor, an affine type theory that adds a modal potential type plus a graded cost monad and refinements, and proves soundness with a Kripke… | ||
| Research as a collaborative effort | PLMW @ POPL 2020 | 2020-01-21 |
Research collaboration is practical: start by starting with your advisor to learn durable technical techniques (not just a narrow problem), read papers to map… | ||
| Formal Methods and Proofs of Privacy Properties, Part I | Data Privacy: Foundations and Applications Boot Camp | 2019-01-28 |
Three-hour mini-course that claims formal methods can make differentially private algorithms correct by design and by proof, with concrete code and tools. It… | ||
| Formal Methods and Proofs of Privacy Properties, Part II | Data Privacy: Foundations and Applications Boot Camp | 2019-01-28 |
Language called PINQ implements privacy by creating chained agents that track budget and apply Laplace noise to counts after checking budget and throwing an… | ||
| Formal Methods and Proofs of Privacy Properties, Part III | Data Privacy: Foundations and Applications Boot Camp | 2019-01-28 |
Claims a practical verification path for differential privacy by encoding relational proofs into SMT solvers and using approximate probabilistic coupling rules… | ||
| nothing matches | ||