►Guannan Wei
Guannan Wei
Research
Publications
Talks/  Posters
Teaching
Services
Code & Open Source Contribution
Quotes
July 1, 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.

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.

  • 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

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

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

  • 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

Dissertation

Talks/Posters🔗

Teaching🔗

Services🔗

Code & 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