►Guannan Wei
Guannan Wei
Research
Publications
Talks/  Posters
Teaching
Services
Quotes
April 15, 2024

Guannan Wei

Email: guannanwei at purdue.edu
Address: 305 N. University Street, West Lafayette, IN 47907
Blog | Github | Twitter | Google Scholar

• Curriculum Vitae
• Research Statement
• Teaching Statement
• Diversity Statement

I am a postdoctoral researcher at Purdue University, and I obtained my Ph.D. in Computer Science from Purdue University, advised by Tiark Rompf. I received M.S. degree in Computer Science from the University of Utah, advised by Matt Might. I was an intern at SambaNova Systems, Galois, and Baidu.

I occasionally take notes of what I read, collect elegant programs, or post random thoughts in my Blog. I take banal and scenic pictures, see my Instagram and gallery.

I will join Tufts CS as a tenure-track Assistant Professor in Fall 2025. Feel free to reach out if you are interested in working with me.

Research

I study scientific and engineering aspects of programming. My research builds better notions and tools to help people build correct, safe, and fast programs. Specifically, I am interested in type systems, program analysis and verification, language implementation, as well as their applications in quantum computing and smart contracts.

  • Building high-performance program analyzers with metaprogramming and high-level programming abstractions.

    We have developped compilation (ICSE ’23, PEPM ’22, FSE ’21, OOPSLA ’20, OOPSLA ’19), derivation (ICFP ’18), and transformation techniques (OOPSLA ’19) to build correct-by-construction, performant, and flexible program analyzers, enabling to use higher-level abstractions yet without compromising performance or correctness.

    Our recent development of the parallel symbolic-execution compiler GenSym (ICSE ’23) demonstrates efficient (4x vs KLEE, single-thread) execution by compiling to continuation-passing style via the 1st Futamura projection.

  • Designing imperative higher-order languages that statically track aliases, separation, and dependencies.

    We have designed reachability types with a flow-sensitive effect system (OOPSLA ’21), offering programmers Rust-style reasoning principles in more expressive and flexible higher-order languages. Reachability types have been used to guide optimizatoins in graph-based compiler IRs (OOPSLA ’23) and extended with \texttt{F}_{<:}-style type-and-reachability polymorphism (POPL ’24). We have also designed a type system to track storage modes, enabling flexible and efficient memory allocation on the stack (ECOOP ’22)

    We are implementing a prototype programming language Diamond with \texttt{F}_{<:}-style precise and polymorphic reachability types.

Publications

Drafts

  1. Escape with Your Self: Expressive Reachability Types with Sound and Decidable Bidirectional Type Checking
    Songlin Jia, Guannan Wei, Siyuan He, Yueyang Tang, Yuyan Bao, Tiark Rompf
    Under submission
    [arxiv]

  2. Modeling Reachability Types with Logical Relations
    Yuyan Bao, Guannan Wei, Oliver Bračevac, Tiark Rompf
    Under submission
    [arxiv]

  3. 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]

Conference/Workshop Papers

  1. 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, Demark

  2. 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] [artifact]

  3. 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] [acm dl] [arxiv] [artifact]

  4. 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]

  5. 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]

  6. 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]

  7. 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]

  8. 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]

  9. 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]

  10. 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]

  11. 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]

  12. 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]

  13. 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]

  14. 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]

  15. 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]

  16. 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

Talks/Posters

Teaching

Services

Open Source Contribution

Quotes

Keep fun in computing — Alan Perlis

On the separation of practical and theoretical work — Christopher Strachey

“The struggle itself is enough to fill a man’s heart. One must imagine Sisyphus happy.” — Albert Camus