design type systems, build compilers, verify programs
Email: jia137 at purdue.edu
Education
Department of Computer SciencePh.D. in Computer Science
- Committee: Tiark Rompf (advisor), Benjamin Delaware, Suresh Jagannathan, and Tianyi Zhang
School of Electronic Information and Electrical EngineeringB.Eng. in Information Security
Publication
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
Proceedings of the ACM on Programming Languages, Volume 10, Issue PLDI, 2026
Typestate via Revocable Capabilities
Songlin Jia, Craig Liu, Siyuan He, Haotian Deng, Yuyan Bao, Tiark Rompf
Proceedings of the ACM on Programming Languages, Volume 10, Issue PLDI, 2026
When Lifetimes Liberate: A Type System for Arenas with Higher-Order Reachability Tracking
Siyuan He, Songlin Jia, Yuyan Bao, Tiark Rompf
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
Proceedings of the ACM on Programming Languages, Volume 9, Issue OOPSLA2, 2025
Complete the Cycle: Reachability Types with Expressive Cyclic References
Haotian Deng, Siyuan He, Songlin Jia, Yuyan Bao, Tiark Rompf
Proceedings of the ACM on Programming Languages, Volume 9, Issue OOPSLA2, 2025
Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs
Guannan Wei, Oliver Bračevac, Songlin Jia, Yuyan Bao, and Tiark Rompf
Proceedings of the ACM on Programming Languages, Volume 8, Issue POPL, 2024
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, and Tiark Rompf
Proceedings of the ACM on Programming Languages, Volume 7, Issue OOPSLA2, 2023
Compiling Parallel Symbolic Execution with Continuations
Guannan Wei, Songlin Jia, Ruiqi Gao, Haotian Deng, Shangyin Tan, Oliver Bračevac, and Tiark Rompf
IEEE/ACM International Conference on Software Engineering (ICSE), 2023
Annotating, Tracking, and Protecting Cryptographic Secrets with CryptoMPK
Xuancheng Jin, Xuangan Xiao, Songlin Jia, Wang Gao, Dawu Gu, Hang Zhang, Siqi Ma, Zhiyun Qian, and Juanru Li
IEEE Symposium on Security and Privacy (SP), 2022
Accelerating SM2 Digital Signature Algorithm Using Modern Processor Features
Long Mai, Yuan Yan, Songlin Jia, Shuran Wang, Jianqiang Wang, Juanru Li, Siqi Ma, and Dawu Gu
International Conference on Information and Communication Security (ICICS), 2019
Work Experience
Applied Scientist Intern, Automated Reasoning
- Delivered tools to solution architects to help identify resilience issues of cloud services at design time;
Applied Scientist Intern, CodeWhisperer
- Fine-tuned language models for code compilation, decompilation, and optimization;
Teaching, Services, and Mentoring
- CS352 & CS502, Compiling and Programming Systems (Scala)2023S,F, 2024F, 2025F, 2026S
- CS565, Programming Languages (Coq, Dafny)2022F, 2025S
- Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)2025, 2026
- Symposium on Principles of Programming Languages (POPL)2025
- International Conference on Functional Programming (ICFP)2024
- Craig Liu, Typestate via Revocable Capabilities (PLDI'26); undergraduate → Ph.D. student at UC Berkeley2025-2026
Talks
- Conference on Programming Language Design and Implementation (PLDI)Boulder, CO; Jun 2026
- Conference on Programming Language Design and Implementation (PLDI)Boulder, CO; Jun 2026
- Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)Pasadena, CA; Oct 2024
Awards & Honors
- Merit Recognition Award for Research, Purdue University West Lafayette, IN; 2024
- Scholarship for Excellent Students, SJTU Shanghai, China; 2017
- First Prize, National Olympiad in Informatics in Provinces (NOIP) Sichuan, China; 2014
Skills
| Programming Languages | Pascal, C/C++, C#, Python, Java, Scala, TypeScript, F# |
| Web Development | HTML/JS/CSS, Vue.js, jQuery, Flask, Django |
| Performance Tuning | C, Assembly (x86, aarch64), OpenMP, MPI |
| Compiler Frameworks | Clang/LLVM, TVM, (Mini)Scala |
| Theorem Proving | Rocq, Lean, Dafny, Boogie |
| Natural Languages | English (fluent), Chinese (native) |