Steve Zdancewic
where else to find them
what they talk about
all 6 in the filters
where they keep going back
- POPL5 editions2021–2026
- OOPSLA3 editions2021–2025
- PLDI Workshop Honoring Andreas Podelski2 editions2025–2026
all 8 in the filters
on a stage with
all 34 in the filters
who talks about the same things
- Nick Rioux5 talks
- Yizhou Zhang13 talks
- Deepak Garg18 talks
- Nada Amin26 talks
- Nadia Polikarpova24 talks
- Amal Ahmed25 talks
| title | conference | date |
|---|---|---|
| Compiling to Recurrent Neurons | PLDI 2026 | 2026-06-15 |
Defines a linearly typed higher-order language Cajal(N) that compiles iteration and conditionals into matrices realized as recurrent neurons, proves a compiler… | ||
| Compiling to Linear Neurons | POPL 2026 | 2026-01-11 |
Claims a typed linear language called Cajal compiles discrete programs into linear neurons by translating conditionals into soft branching linear maps, with a… | ||
| Opportunistically Parallel Lambda Calculus | OOPSLA 2025 | 2025-10-16 |
Proposes an evaluation strategy and core calculus (Opportunistic Lambda Calculus) that dispatches independent external calls as holes, resolves them… | ||
| Functional Meaning for Parallel Streaming | PLDI 2025 | 2025-06-16 |
A core language called λ∨ formalizes deterministic parallel streaming by making values monotonically increase under a streaming order that matches Scott… | ||
| Vellvm: Formalizing the Informal | CoqPL 2025 | 2025-01-25 |
Formal Coq semantics for a large subset of LLVM IR uses interaction trees (coinductive freemonads) plus event handlers to capture nondeterminism and a… | ||
| Welcome from the general chair | POPL 2025 | 2025-01-19 |
Conference runs with three colocated symposia, nine workshops and five tutorials, plus many student and social events; reception at 6:00, SRC poster session… | ||
| Optimal Program Synthesis via Abstract Interpretation | POPL 2024 | 2024-01-14 |
The paper presents a synthesis framework that finds numerically parameterized programs optimally by enumerating generalized partial programs and running A… | ||
| Granite: Compositional Functional Logic Programming | HOPE 2023 | 2023-09-04 |
Granite puts a join as semilattice primitive at the language core, letting parallel executions merge by associative commutative idempotent joins; it encodes… | ||
| CPP Business Meeting | CPP 2023 | 2023-01-16 |
Conference reports concrete numbers: 53 submissions, 25 accepted after a two‑month light double‑blind review with 33 PC members and about 20 external… | ||
| A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F... | POPL 2023 | 2023-01-15 |
Presents F⋈, a small core language that lets intersection types, union types and overloaded functions coexist with a deterministic merge operator by enforcing… | ||
| Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in C... | POPL 2023 | 2023-01-15 |
Introduces a coinductive tree datatype and a ctrees monad in Coq that models nondeterminism, recursion, and effects by three node kinds: external events and… | ||
| C4: verified transactional objects | OOPSLA 2022 | 2022-12-05 |
C4 claims a mechanized, compositional way to prove both linearizability and strict serializability and to stitch those proofs together for mixed… | ||
| Formal Reasoning about Layered Monadic Interpreters | ICFP 2022 | 2022-09-11 |
Extends the Coq interaction trees (ITrees) library to characterize a class of interpretable monads obtained by applying monad transformers to ITrees, gives… | ||
| A Type System for Extracting Functional Specifications from Memory-Safe Imperative Programs | OOPSLA 2021 | 2021-10-17 |
A memory-safe Rust-like type system called Heapster typechecks LLVM IR and extracts Coq functions that represent imperative behavior without pointer reasoning… | ||
| Dijkstra Monads Forever | POPL 2021 | 2021-01-17 |
Extends Dijkstra monads to termination‑sensitive specifications for interactive, possibly nonterminating programs by adding two base spec monads (a delay spec… | ||
| Computation Focusing | ICFP 2020 | 2020-08-23 |
Presents a focused polymorphic call-by-push-value calculus and proves computational completeness: every well-typed term has a βη-equivalent focused… | ||
| Vellvm - Verifying the LLVM | Strange Loop 2018 | 2018-09-26 |
Vellvm formalizes LLVM IR semantics in Coq, extracts an OCaml interpreter that runs real .ll files, and implements a verified register‑promotion pipeline (a… | ||
| nothing matches | ||