Guannan Wei
where else to find them
what they talk about
all 8 in the filters
where they keep going back
- OOPSLA5 editions2020–2025
- PLDI Workshop Honoring Andreas Podelski2 editions2024–2026
all 7 in the filters
on a stage with
all 26 in the filters
who talks about the same things
- Tiark Rompf24 talks
- Songlin Jia6 talks
- Yuyan Bao8 talks
- Oliver Bračevac9 talks
- Yizhou Zhang13 talks
- Derek Dreyer35 talks
| title | conference | date |
|---|---|---|
| Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for(…) | PLDI 2026 | 2026-06-15 |
Presents an algorithmic design for reachability types that proves sound and decidable bidirectional typing and avoidance, mechanized in Lean 4 and accompanied… | ||
| Efficient Concolic Execution of WebAssembly by Compilation and Snapshot Reuse | WebAssembly Workshop @ ICFP/SPLASH 2025 | 2025-10-16 |
Claims a concolic engine that compiles a CPS-based Wasm concolic interpreter to C++ via partial evaluation (LMS), producing an executable that combines no… | ||
| Modeling Reachability Types with Logical Relations -- Semantic Type Soundness,(…) | OOPSLA 2025 | 2025-10-16 |
Presents a formal logical-relations model for reachability types that augments standard relations with relational store typing to localize heap reasoning, and… | ||
| Programming Large Language Models with Algebraic Effect Handlers and the Selection Monad | LMPL 2025 | 2025-10-12 |
Pangolin models LLM calls as algebraic effects and uses a selection monad to search and score nondeterministic outputs; handlers expose a multi‑shot… | ||
| Hallucination-Resilient LLM-Driven Sound and Tunable Static Analysis | LMPL 2025 | 2025-10-12 |
Claims a sound, LLM-driven static analyzer called LLMAAM that delegates abstract address allocation to an LLM while guaranteeing soundness by construction and… | ||
| A Big-Step Compositional Continuation-Passing Semantics for WebAssembly | WAW 2025 | 2025-01-20 |
Presents a compositional CPS semantics for a WebAssembly subset that replaces the official small-step reduction with a big-step, tail-recursive interpreter… | ||
| Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in(…) | OOPSLA 2024 | 2024-10-20 |
Presents a type system that adds a freshness qualifier to reachability types so newly allocated values remain distinct until substituted, enabling precise… | ||
| ParDiff: Practical Static Differential Analysis of Network Protocol Parsers | OOPSLA 2024 | 2024-10-20 |
ParDiff statically extracts protocol-format constraints from C implementations, extracts finite-state machines ordered by buffer indices, and uses bisimulation… | ||
| Consolidating Smart Contracts with Behavioral Contracts | PLDI 2024 | 2024-06-24 |
ConSol extends Solidity with a transpiler that attaches behavioral contracts to first-class addresses by expanding 160-bit addresses into a guarded address… | ||
| Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in ... | POPL 2024 | 2024-01-14 |
Introduces a new freshness qualifier (diamond) that marks allocations whose reachability may materialize later, and designs two calculi (λ✦ and F✦ calculi)… | ||
| Graph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Af... | OOPSLA 2023 | 2023-10-23 |
A typed graph IR combines reachability types with an effect system to compute precise, flow-sensitive effect dependencies without CFA by doing type-based… | ||
| Partially Evaluating Symbolic Interpreters for All | PEPM 2022 | 2022-01-17 |
Builds staged symbolic interpreters with Lightweight Modular Staging (LMS) to compile concolic and call‑chain backward symbolic execution for an LLVM‑style IR… | ||
| Reachability Types: Tracking Aliasing and Separation in Higher-Order Functional Programs | OOPSLA 2021 | 2021-10-17 |
New type system lambda assigns reachability qualifiers to expressions to track exact alias sets, enforces separation for higher-order functions with function… | ||
| Compiling Symbolic Execution with Staging and Algebraic Effects | OOPSLA 2020 | 2020-11-15 |
Claims a first Futamura projection for symbolic interpreters and shows a pipeline that stages a definitional interpreter (Scala + Freer monads + LMS) to… | ||
| nothing matches | ||