Speaker

Guannan Wei

Abstract

In this talk, I will present an overview of my research, which provides novel directions for building correct, safe, and performant software systems through the use of programming languages and compiler techniques. In the first part of the talk, I will introduce reachability type systems, a family of static type systems aiming at tracking sharing, separation, and side-effects in higher-order imperative programs. Reachability types provide a smooth integration of Rust-style ownership types with higher-level programming abstractions, such as first-class functions. In the second part, I will discuss how metaprogramming techniques can aid in building correct, flexible, and performant program analyzers. I will introduce GenSym, a parallel symbolic-execution compiler derived from a high-level definitional symbolic interpreter using program generation techniques. GenSym generates code in continuation-passing style to perform parallel symbolic execution of LLVM IR programs, and significantly outperforms similar state-of-the-art tools. The talk will also cover my future research agenda, such as applications of reachability types in quantum computing.

Bio

Guannan Wei is currently a postdoctoral researcher at Purdue University. His research interests lie in programming languages and software engineering, including designing better programming languages and program analyzers with high-level programming abstractions. His contributions have been published in flagship programming languages and software engineering venues, such as POPL, OOPSLA, ICFP, ECOOP, ICSE, and ESEC/FSE. Guannan received his PhD degree (2023) in Computer Science from Purdue University, advised by Tiark Rompf. He obtained his MS degree in Computer Science from the University of Utah. He is the 2022 recipient of the Maurice H. Halstead Memorial Award for Software Engineering Research. More of Guannan’s work can be found at continuation.passing.style.