Guannan Wei🔗

• Neurosymbolic Code Auditing
  Chengpeng Wang, Zhuo Zhang, Xiangzhe Xu, Mingwei Zheng, Guannan Wei, Xiangyu Zhang
  Foundations and Trends in Programming Languages (To appear). 2026
  [preprint]

• Compiling Concolic Execution with Staging, Continuations, and Snapshots
  Dinghong Zhong, Alex Bai, Mikail Khan, Guannan Wei
  OOPSLA 2026 (To appear)
  

• When Do Staging Annotations Preserve Semantics? Mechanizing Typed Semantics-Preserving Multi-Stage Programming with Let-Insertion
  Jun Tan, Guannan Wei
  OOPSLA 2026 (To appear)
  [arxiv] [artifact]

• Let It Be Optimized: Building Multi-Stage Evaluators with Let-Insertion and Optimizations in Small Pieces (Functional Pearl)
  Guannan Wei, Jun Tan, Dinghong Zhong
  Proceedings of the ACM on Programming Languages, Volume 10 (ICFP 2026). IN, USA
  [pdf] [artifact]

• Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for Reachability Types
  Songlin Jia, Guannan Wei, Siyuan He, Yuyan Bao, Tiark Rompf
  Proceedings of the ACM on Programming Languages, Volume 10 (PLDI 2026). Boulder, CO, USA
  [pdf] [acm dl] [artifact]

• Hallucination-Resilient LLM-Driven Sound and Tunable Static Analysis – A Case of Higher-Order Control-Flow Analysis (Position paper)
  Guannan Wei, Zhuo Zhang, Caterina Urban
  The 1st International Workshop on Language Models and Programming Languages (LMPL), co-located with SPLASH/ICFP 2025. Singapore
  [pdf] [acm dl] [artifact]

• Programming Large Language Models with Algebraic Effect Handlers and the Selection Monad (Position paper)
  Shangyin Tan, Guannan Wei, Koushik Sen, Matei Zaharia
  The 1st International Workshop on Language Models and Programming Languages (LMPL), co-located with SPLASH/ICFP 2025. Singapore
  [pdf]

• Modeling Reachability Types with Logical Relations – Semantic Type Soundness, Termination, Effect Safety, and Equational Theory
  Yuyan Bao, Songlin Jia, Guannan Wei, Oliver Bračevac, Tiark Rompf
  Proceedings of the ACM on Programming Languages, Volume 9 (OOPSLA 2025). Singapore
  [arxiv] [acm dl] [artifact]

• Reconstructing Continuation-Passing Semantics for WebAssembly
  Guannan Wei, Alex Bai, Dinghong Zhong, Jiatai Zhang
  Proceedings of the 26th International Symposium on Trends in Functional Programming (TFP 2025). Oxford, UK
  [pdf] [springer] [artifact]

• Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs
  Guannan Wei, Oliver Bračevac, Songlin Jia, Yuyan Bao, Tiark Rompf
  Proceedings of the ACM on Programming Languages, Volume 8 (POPL 2024). London, United Kingdom
  [pdf] [appendix] [acm dl] [arxiv] [artifact]

• Consolidating Smart Contracts with Behavioral Contracts
  Guannan Wei, Danning Xie, Wuqi Zhang, Yongwei Yuan, Zhuo Zhang* (* corresponding author)
  Proceedings of the ACM on Programming Languages, Volume 8 (PLDI 2024). Copenhagen, Denmark
  [pdf] [acm dl] [artifact]

• ParDiff: Practical Static Differential Analysis of Network Protocol Parsers
  Mingwei Zheng, Qingkai Shi, Xuwei Liu, Xiangzhe Xu, Le Yu, Congyu Liu, Guannan Wei, Xiangyu Zhang
  Proceedings of the ACM on Programming Languages, Volume 8 (OOPSLA 2024). Pasadena, CA, USA
  Distinguished Paper Award
  [pdf] [acm dl] [artifact]

• Compiling Parallel Symbolic Execution with Continuations
  Guannan Wei, Songlin Jia, Ruiqi Gao, Haotian Deng, Shangyin Tan, Oliver Bračevac, Tiark Rompf
  The 45th International Conference on Software Engineering (ICSE 2023)
  [pdf] [ieee] [artifact]

• Graph IRs for Impure Higher-Order Languages – Making Aggressive Optimizations Affordable with Precise Effect Dependencies
  Oliver Bračevac, Guannan Wei, Songlin Jia, Supun Abeysinghe, Yuxuan Jiang, Yuyan Bao, Tiark Rompf
  Proceedings of the ACM on Programming Languages, Volume 7 (OOPSLA 2023). Cascais, Portugal
  [pdf] [acm dl]

• Metaprogramming Program Analyzers
  Guannan Wei
  PhD Dissertation. Purdue University. 2023
  [pdf]

• What If We Don’t Pop the Stack? The Return of Second-Class Values
  Anxhelo Xhebraj, Oliver Bračevac, Guannan Wei, Tiark Rompf
  Proceedings of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Berlin, Germany
  [pdf] [dagstuhl] [artifact]

• Towards Partially Evaluating Symbolic Interpreters for All
  Shangyin Tan, Guannan Wei, Tiark Rompf
  ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM), co-located with POPL 2022. Philadelphia, PA, USA
  [pdf] [bib]

• Reachability Types: Tracking Aliasing and Separation in Higher-Order Functional Programs
  Yuyan Bao, Guannan Wei, Oliver Bračevac, Yuxuan Jiang, Qiyang He, Tiark Rompf
  Proceedings of the ACM on Programming Languages, Volume 5 (OOPSLA 2021). Online/Chicago, IL, USA
  [pdf] [acm dl] [artifact]

• LLSC: A Parallel Symbolic Execution Compiler for LLVM IR (Tool Demonstration)
  Guannan Wei, Shangyin Tan, Oliver Bračevac, Tiark Rompf
  Proceedings of the 29th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE 2021)
  [pdf] [acm dl] [demo]

• Compiling Symbolic Execution with Staging and Algebraic Effects
  Guannan Wei, Oliver Bračevac, Shangyin Tan, Tiark Rompf
  Proceedings of the ACM on Programming Languages, Volume 4 (OOPSLA 2020). Online
  [pdf] [acm dl] [artifact]

• Staged Abstract Interpreters: Fast and Modular Whole-Program Analysis via Meta-Programming
  Guannan Wei, Yuxuan Chen, Tiark Rompf
  Proceedings of the ACM on Programming Languages, Volume 3 (OOPSLA 2019). Athens, Greece
  [pdf] [acm dl] [artifact]

• Precise Reasoning with Structured Time, Structured Heaps, and Collective Operations
  Grégory Essertel, Guannan Wei, Tiark Rompf
  Proceedings of the ACM on Programming Languages, Volume 3 (OOPSLA 2019). Athens, Greece
  [pdf] [acm dl] [artifact]

• BDA: Practical Dependence Analysis for Binary Executables by Unbiased Whole-program Path Sampling and Per-path Abstract Interpretation
  Zhuo Zhang, Wei You, Guanhong Tao, Guannan Wei, Yonghwi Kwon, Xiangyu Zhang
  Proceedings of the ACM on Programming Languages, Volume 3 (OOPSLA 2019). Athens, Greece
  Distinguished Paper Award
  [pdf] [acm dl] [artifact]

• Towards Verified Binary Raising
  Joe Hendrix, Guannan Wei, Simon Winwood
  Workshop on Instruction Set Architecture Specification, co-located with ITP 2019. Portland, OR, USA
  [pdf] [bib]

• Graph Neural Reasoning for 2-Quantified Boolean Formula Solvers
  Zhanfu Yang, Fei Wang, Ziliang Chen, Guannan Wei, Tiark Rompf
  Workshop on Learning and Reasoning with Graph-Structured Representations, co-located with ICML 2019. Long Beach, CA, USA
  [pdf] [bib]

• Refunctionalization of Abstract Abstract Machines (Functional Pearl)
  Guannan Wei, James M. Decker, Tiark Rompf
  Proceedings of the ACM on Programming Languages, Volume 2 (ICFP 2018). St. Louis, MO, USA
  [pdf] [acm dl] [artifact]

• Snek: Overloading Python Semantics via Virtualization
  James M. Decker, Dan Moldovan, Andrew A. Johnson, Guannan Wei, Fei Wang, Grégory Essertel, Alexander B. Wiltschko, Tiark Rompf
  [pdf]

• Software Foundations (Chinese version)

• Workshop on Virtual Machines and Language Implementations (VMIL) ’26

• ACM International Conference on Functional Programming (ICFP) ’26 SRC

• ACM Conference on Programming Languages Design and Implementation (PLDI) ’26 SRC

• International Conference on AI-powered Software (AIWare) ’26

• Workshop on Explainable and Reliable Software Systems (EXPRESS) ’26

• Workshop on Partial Evaluation and Program Manipulation (PEPM) ’26

• Trends in Functional Programming in Education (TFPIE) ’26

• ACM Conference on Programming Languages Design and Implementation (PLDI) ’25

• ACM Conference on Object-Oriented Programming and Systems (OOPSLA) ’25

• ACM International Conference on Functional Programming (ICFP) ’25

• Generative Code Intelligence Workshop (GeCoIn) ’25

• miniKanren and Relational Programming Workshop (miniKanren) ’25

• Scala Workshop ’25

• New England Programming Languages and Systems Symposium (NEPLS) ’25Spring

• Symposium on Dependable Software Engineering Theories, Tools and Applications (SETTA) ’25

• Trends in Functional Programming in Education (TFPIE) ’25

• Symposium on Dependable Software Engineering Theories, Tools and Applications (SETTA) ’24 (Distinguished Reviewer)

• International Conference on Computer and Communication Quality (ICCQ) ’24

• International Conference on Computer and Communication Quality (ICCQ) ’23

• Workshop on Virtual Machines and Language Implementations (VMIL) ’21

  “I think that it’s extraordinarily important that we in computer science keep fun in computing. When it started out, it was an awful lot of fun. Of course, the paying customers got shafted every now and then, and after a while we began to take their complaints seriously. We began to feel as if we really were responsible for the successful, error-free perfect use of these machines. I don’t think we are. I think we’re responsible for stretching them, setting them off in new directions, and keeping fun in the house. I hope the field of computer science never loses its sense of fun. Above all, I hope we don’t become missionaries. Don’t feel as if you’re Bible salesmen. The world has too many of those already. What you know about computing other people will learn. Don’t feel as if the key to successful computing is only in your hands. What’s in your hands, I think and hope, is intelligence: the ability to see the machine as more than when you were first led up to it, that you can make it more.”

  “It has long been my personal view that the separation of practical and theoretical work is artificial and injurious. Much of the practical work done in computing, both in software and in hardware design, is unsound and clumsy because the people who do it have not any clear understanding of the fundamental design principles of their work. Most of the abstract mathematical and theoretical work is sterile because it has no point of contact with real computing.”