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]

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

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

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 Proceedings of the ACM on Programming Languages, Volume 8, Issue POPL, 2024
[doi]

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 Proceedings of the ACM on Programming Languages, Volume 7, Issue OOPSLA2, 2023
[doi]

Compiling Parallel Symbolic Execution with Continuations
Guannan Wei, Songlin Jia, Ruiqi Gao, Haotian Deng, Shangyin Tan, Oliver Bračevac, and Tiark Rompf
in IEEE/ACM International Conference on Software Engineering (ICSE), 2023
[doi]

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

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