Deepak Garg
where else to find them
no profile links on file
what they talk about
all 9 in the filters
where they keep going back
- POPL4 editions2021–2026
- OOPSLA4 editions2022–2025
- PLDI Workshop Honoring Andreas Podelski2 editions2024–2025
all 8 in the filters
on a stage with
all 42 in the filters
who talks about the same things
- Steve Zdancewic19 talks
- Michael Sammler16 talks
- Lars Birkedal35 talks
- Amal Ahmed25 talks
- Michel Steuwer17 talks
- Tiark Rompf24 talks
| title | conference | date |
|---|---|---|
| A Recipe for Modular Verification of Generic Tree Traversals | CPP 2026 | 2026-01-12 |
Presents a concrete verification recipe that models traversal state with a zipper with shadow and characterizes step types as action and silent steps, yielding… | ||
| Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic(…) | POPL 2026 | 2026-01-11 |
Shows a hardening compiler that makes a C‑like source (Rec) robustly safe only after compilation to a CHERI‑style capability machine (Cap); proves a separation… | ||
| Non-interference Preserving Optimising Compilation | OOPSLA 2025 | 2025-10-16 |
Introduces hyperproperty simulations as a new secure-compilation framework that models preservation of arbitrary k‑hyperproperties and proves a generic… | ||
| Fusing Session-Typed Concurrent Programming into Functional Programming | ICFP 2025 | 2025-10-12 |
FuSes embeds a session-typed process calculus inside a pure functional language and ships a formal type system with operational semantics and a machine-checked… | ||
| RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free(…) | PLDI 2025 | 2025-06-16 |
Claims a machine‑checked end‑to‑end proof that an interrupt‑free, fixed‑priority, non‑preemptive scheduler meets response‑time bounds by connecting program… | ||
| A Semantic Approach to Robust Property Preservation | PriSC 2025 (with POPL 2025) | 2025-01-20 |
Proposes a semantic reduction of robust property preservation: replace hard syntactic backtranslation with a backtranslation between semantic domains, so… | ||
| Non-Interference Preserving and Optimising Compilation with Hyperproperty Simulations | PriSC 2025 (with POPL 2025) | 2025-01-20 |
Presents a formal framework that generalizes compiler simulation proofs to arbitrary k‑trace hyperproperties and claims preservation of… | ||
| A modal type-theory of expected cost in higher-order probabilistic programs | OOPSLA 2024 | 2024-10-20 |
pλ-amor is a graded modal type theory that encodes probabilities, potentials and expected cost at the type level and proves bounds for higher-order… | ||
| 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… | ||
| Compositional Security Definitions for Higher-Order Where Declassification | OOPSLA 2023 | 2023-10-23 |
Defines a compositional security notion for where declassification in higher-order languages by building an indistinguishability logical relation that stops… | ||
| DimSum: A Decentralized Approach to Multi-language Semantics and Verification | POPL 2023 | 2023-01-15 |
DimSum presents a decentralized method that avoids fixing a source language, memory model, or closed set of languages by giving each language a… | ||
| BFF: Foundational and Automated Verification of Bitfield-Manipulating Programs | OOPSLA 2022 | 2022-12-05 |
A foundational, automated verifier encodes common bitfield patterns as structured bit vectors and implements partial, semantics-preserving operations (masking… | ||
| Pirouette: Higher-Order Typed Functional Choreographies | POPL 2022 | 2022-01-16 |
Pirouette is a choreographic language that compiles a single higher-order functional program into one program per node via endpoint projection, with two… | ||
| Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI | POPL 2022 | 2022-01-16 |
Paper claims that adding static invariants lets sandboxed code use simple function calls instead of heavyweight wrappers, and implements this end-to-end. A… | ||
| 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… | ||
| Qapla: Policy compliance for database-backed systems | 26th USENIX Security Symposium (USENIX Security '17) | 2017-08-16 |
Qapla is a DB-adapter reference monitor that enforces fine-grained, row-and-column policies by query rewriting: it replaces each table with a subquery… | ||
| Thoth: Comprehensive Policy Compliance in Data Retrieval Systems | USENIX Security '16 | 2016-08-10 |
Thoth enforces data-use policies attached to files, sockets and key-value tuples using process-level information flow control and a declarative policy language… | ||
| nothing matches | ||