Guannan Wei

April 29, 2025

Guannan Wei🔗

Recent:
• Papers/Talks: LIPN Seminar, Wasm Research Day ’25, Wasm Workshop @ POPL’25
• PC Member: GeCoIn ’25, miniKanren ’25, Scala ’25, NEPLS ’25Sp, SETTA ’25, ICFP ’25, TFPIE ’25, PLDI ’25, OOPSLA ’25

I am a postdoctoral researcher in the ANTIQUE team at INRIA and École Normale Supérieure (Paris), working with Caterina Urban. I am also a visiting assistant professor at Tufts University. I obtained my Ph.D. in Computer Science from Purdue University (advised by Tiark Rompf), and M.S. from the University of Utah (advised by Matt Might).

I study the scientific and engineering aspects of software systems and programming. Driven by a fascination with how programming languages allow people creating abstractions and communicating ideas, my research aims to develop novel notions and tools that empower people to build correct, safe, and efficient software.

I will join CS@Tufts as an Assistant Professor in Fall 2025. If you are interested in working with me in PL, formal methods, or software engineering, feel free to reach out!

Research🔗

I am generally interested in type systems, program analysis/verification/testing, interpreters and compilers, metaprogramming, as well as their applications. Some of my ongoing research themes:

Metaprogramming program analyzers.
[ICSE ’23, PEPM ’22, FSE ’21, OOPSLA ’20, OOPSLA ’19a, OOPSLA ’19b, ICFP ’18] [More]
How can we write programs that generate program analyzers? My PhD work developed metaprogramming techniques to build correct-by-construction, performant, and flexible analyzers. I developed compilation [ICSE ’23, PEPM ’22, FSE ’21, OOPSLA ’20, OOPSLA ’19a], derivation [ICFP ’18], and transformation [OOPSLA ’19b] techniques for program analysis.
We build a compiler GenSym [ICSE ’23] for parallel, efficient symbolic-execution (even 4X faster than KLEE with single-thread). GenSym compiles parallel symbolic-execution to continuation-passing style by Futamura projection, only taking the effort of implementing a symbolic interpreter.
Languages for tracking lifetime, sharing, and separation.
[POPL ’24, OOPSLA ’23, ECOOP ’22, OOPSLA ’21] [More]
While Rust has achieved significant success in low-level programming, I’m interested in bringing the benefits of Rust-style reasoning to functional languages with with side-effects and pervasive functional/type abstractions.
We designed reachabitly type systems to track resource sharing and separation, offering Rust-style reasoning principles in expressive higher-order languages [Diamond, POPL ’24, OOPSLA ’21], flexible and efficient stack-based memory management based on second-class values [ECOOP ’22], and aggressive optimizations in graph-based compiler IRs [OOPSLA ’23].

Publications🔗

Recent Drafts

Avoid Arguments and Escape with Your Self: Expressive Subtyping and Decidable Bidirectional Checking for Reachability Types
Songlin Jia, Guannan Wei, Siyuan He, Yueyang Tang, Yuyan Bao, Tiark Rompf
Under submission
[arxiv]
Modeling Reachability Types with Logical Relations
Yuyan Bao, Songlin Jia, Guannan Wei, Oliver Bračevac, Tiark Rompf
Under submission
[arxiv]

Conference/Workshop Papers

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] [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
[pdf] [acm dl] [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]
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]
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]
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
[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]

Dissertation

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

Manuscripts

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]

Talks🔗

Polymorphic Reachability Types and Effects: An Overview
LIPN (Laboratoire d’Informatique de Paris Nord), Univ. Sorbonne Paris Nord. Mar 2025 [slides]
Reconstructing Continuation-Passing Semantics for WebAssembly
WebAssembly Research Day. Hosted by Fastly. Feb 2025 [slides]
The WebAssembly Workshop (WAW), co-located with POPL. Denver, CO. Jan 2025 [slides]
Metaprogramming Program Analyzers
ANTIQUE Seminar. INRIA/ENS-PSL Paris. Oct 2024 [slides]
Consolidating Smart Contracts with Behavioral Contracts
PLDI 2024. Copenhagen, Denmark. June 2024 [slides]
Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs
POPL 2024. London, UK. Jan 2024 [slides]
Midwest Programming Languages Summit (MWPLS). Ann Arbor, MI. Oct 2023 [poster]
Compiling and Controlling Symbolic Execution
Northeastern University Programming Languages Seminar. Boston, MA. Dec 2023 [slides]
Midwest Programming Languages Summit (MWPLS). Ann Arbor, MI. Oct 2023 [slides]
Purdue PL Seminar. West Lafayette, IN. Dec 2022 [slides]
Compiling Parallel Symbolic Execution with Continuations
ICSE 2023. Remote. May 2023 [slides]
Reachability Types: Tracking Aliasing and Separation in Higher-Order Functional Programs
OOPSLA 2021. Chicago, IL. Oct 2021 [poster]
LLSC: A Parallel Symbolic Execution Compiler for LLVM IR
ESEC/FSE 2021. Online. Aug 2021 [slides]
Compiling Symbolic Execution with Staging and Algebraic Effects
OOPSLA 2020. Online. Nov 2020 [slides]
Metaprogramming for Program Analyzers
PurPL Retreat. Online. Aug 2020 [slides]
Staged Abstract Interpreters
OOPSLA 2019. Athens, Greece. Oct 2019 [slides]
Refunctionalization of Abstract Abstract Machines (Functional Pearl)
ICFP 2018. St. Louis, MO. Sep 2018 [slides][poster]
Precise Reasoning with Structured Heaps and Collective Operations à la Map/Reduce
Purdue PL Seminar. West Lafayette, IN. Jan 2018 [slides]
Midwest Programming Languages Summit (MWPLS). Bloomington, IN. Dec 2017 [slides]
Huawei Research Summit. Urbana-Champaign, IL. Mar 2018 [slides]

Mentoring🔗

Undergraduate Students

Alex Bai, Tufts University, Fall 2024 -
Mikail Khan, Purdue University, Fall 2022 - Spring 2024 (Next step: PhD student at CMU)
Shangyin Tan, Purdue University, Summer 2020 - Fall 2021 (Next step: PhD student at UC Berkeley)
Yuxuan Chen, Purdue University, Fall 2018 (Next step: Software Engineer at Meta)

Teaching🔗

Co-instructor, CS352 Compilers: Principles and Practice (undergraduate)
Spring 2024, Purdue University
Lead Teaching Assistant, CS352 Compilers: Principles and Practice (undergraduate)
Spring 2020, Purdue University [testimonials]
  “Guannan you are a real homie, thanks for carrying the course and helping out all the students who were lost as hell – please know that your help in this class is probably what got everyone through it, you are a blessed human being thanks for your existence :)”
  “Guannan was patient and very helpful with the projects. I’m really glad he was my TA because he helped a lot along the way.”
  “Guannan is a god on Piazza.”
  “Guannan is a great TA and is very talented. He was great at answering questions during the lab session and helping students debug their code, especially since most of us were using a language we had never used before. He was also very active on Piazza, helping me and other students whenever we had questions about the projects or lecture.”
Teaching Assistant, CS502 Compilers: Principles and Practice (graduate)
Fall 2019, Purdue University
Lab Instructor, CS252 System Programming (undergraduate)
Fall 2017, Spring 2018, Purdue University

Services🔗

Program Committee Member: Generative Code Intelligence Workshop (GeCoIn) 2025, miniKanren Workshop 2025, Scala Workshop 2025, NEPLS 2025 Spring, SETTA 2025, ICFP 2025, TFPIE 2025, PLDI 2025, OOPSLA 2025, SETTA 2024 (Distinguished Reviewer Award), ICCQ 2024, ICCQ 2023, VMIL 2021, EuroSys Shadow 2021
Reviwer: TOSEM 2024, ICFP 2022, ISSTA 2021, ICLR 2019
Artifact Evaluation Committee Member: ISSTA 2024, OOPSLA 2024, POPL 2024, ICFP 2023, PLDI 2023, POPL 2023, PLDI 2022, PLDI 2021, ICFP 2021, ISSTA 2021, OOPSLA 2020, ICFP 2020, CAV 2020, ICFP 2019
Student Volunteer: POPL 2023, ICFP 2019, MWPLS & PurPL Fest 2019
Translator: Software Foundations (Chinese edition)

Code🔗

GenSym: a compiler for parallel symbolic-execution of LLVM IR
Diamond language: a prototype language with the polymorphic reachability type system
Reachability types: mechanizations of various calculi in Coq
lms-clean: the Lightweight Modular Staging framework

Quotes🔗

Keep fun in computing — Alan Perlis

On the separation of practical and theoretical work — Christopher Strachey

Page generated using Racket and Scribble.

	Research
	Publications
	Talks
	Mentoring
	Teaching
	Services
	Code
	Quotes