Songlin Jia is a Ph.D. candidate at Purdue CS. Interested in programming languages, he currently works with Prof. Tiark Rompf. He has been working on a performant, full-fledged symbolic execution engine by staging, and recently its underlying graph IR, and reachability type systems.
Songlin has been a teaching assistant for CS502 Compiling and Programming Systems and CS565 Programming Languages.
Songlin got his bachelor’s degree at Shanghai Jiao Tong University, where he used to work on scientific computing and program analysis.
Recent Publication
Free to Move: Reachability Types with Flow-Sensitive Effects for Safe Deallocation and Ownership Transfer
Haotian Deng, Siyuan He, Songlin Jia, Yuyan Bao, Tiark Rompf
in submission, 2026
Adaptive Proof Refinement with LLM-Guided Strategy Selection
Minghai Lu, Zhe Zhou, Danning Xie, Songlin Jia, Benjamin Delaware, Tianyi Zhang
to be appeared in ASE, 2026
Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for Reachability Types
Songlin Jia, Guannan Wei, Siyuan He, Yuyan Bao, Tiark Rompf
in Proceedings of the ACM on Programming Languages, Volume 10, Issue PLDI, 2026
[doi] [extended] [slides] [artifact]
Typestate via Revocable Capabilities
Songlin Jia, Craig Liu, Siyuan He, Haotian Deng, Yuyan Bao, Tiark Rompf
in Proceedings of the ACM on Programming Languages, Volume 10, Issue PLDI, 2026
[doi] [arxiv] [slides] [artifact]
When Lifetimes Liberate: A Type System for Arenas with Higher-Order Reachability Tracking
Siyuan He, Songlin Jia, Yuyan Bao, Tiark Rompf
in Proceedings of the ACM on Programming Languages, Volume 10, Issue OOPSLA1, 2026
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
in Proceedings of the ACM on Programming Languages, Volume 9, Issue OOPSLA2, 2025
Posts
subscribe via RSS