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

Let Functions Speak: Lightweight Parametric Polymorphism via Domain and Range Types
Siyuan He, Songlin Jia, Tiark Rompf
in submission, 2026
[arxiv]

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
[arxiv]

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
[arxiv]

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] [mechanization]

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] [extended] [slides] [prototype]

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
[doi]

Posts

subscribe via RSS