Education

• Working with Prof. Tiark Rompf on programming languages and compilers;
• Core Courses: Algorithm Design, Analysis, and Implementation (A+), Programming Languages (A+), Distributed Systems (A+);

• Core Courses: Linear Algebra (94), Discrete Mathematics (97), Computer Organization and Architecture (95), Compiler Principles (91), Computer Communication and Network (92.5);
• Experiences in web development, parallel programming, and program analysis;

Publication

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 submission, 2025

Typestate via Revocable Capabilities
Songlin Jia, Craig Liu, Siyuan He, Haotian Deng, Yuyan Bao, Tiark Rompf
in submission, 2025

When Lifetimes Liberate: A Type System for Arenas with Higher-Order Reachability Tracking
Siyuan He, Songlin Jia, Yuyan Bao, Tiark Rompf
in submission, 2025

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, 2025

Adaptive Proof Refinement with LLM-Guided Strategy Selection
Minghai Lu, Zhe Zhou, Danning Xie, Songlin Jia, Benjamin Delaware, Tianyi Zhang
in submission, 2025

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

Complete the Cycle: Reachability Types with Expressive Cyclic References
Haotian Deng, Siyuan He, Songlin Jia, Yuyan Bao, Tiark Rompf
in 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
in ACM-SIGACT Symposium on Principles of Programming Languages (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
in ACM SIGPLAN International Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 2023

Compiling Parallel Symbolic Execution with Continuations
Guannan Wei, Songlin Jia, Ruiqi Gao, Haotian Deng, Shangyin Tan, Oliver Bračevac, and Tiark Rompf
in 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
in 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
in International Conference on Information and Communication Security (ICICS), 2019

Experience

• CS502, Compiling and Programming Systems (Scala), 2022 Fall, 2024 Fall, 2025 Fall;
• CS565, Programming Languages (Coq, Dafny), 2023 Spring & Fall, 2025 Spring;

• Analysis of service resilience using symbolic execution (Astrid);

• Language model for low-level code generation (CodeWhisperer);

• Rebuilt the service management system and optimized its interaction guidance, information layout, and data fetching;
• Leading the 4-per development team, implemented the backend (Django) and contributed to the front-end (Vue.js);