Ph.D. Student
Computer Science Department (CSD)
Carnegie Mellon University (CMU)
Links
Email: yueyao@cs.cmu.edu
GitHub: @tripack45
CV: cv.pdf
I am a 4th year PhD student at Carnegie Mellon University studying programming languages. My research applies semantic methods, most notably the method of logical relations, to interesting applied and theoretical problems pertaining to substructural types and concurrency, including session types. Towards these ends, my research also involves (linear) type theories and mechanizing results in a theorem prover. My research aims to enable the design of practical, multiparadigm languages equipped with sophisticated type systems and strong theoretical guarantees. I am advised by Stephanie Balzer.
Education
Advised by Stephanie Balzer.
Thesis: Work-Efficient Schedulers. Committee: Umut Acar (Chair) and Randal Bryant.
Graduated with distinction.
Professional
Experience
Research
Artifacts
Istari-STC
We mechanized proofs of canonicity for a core dependent type theory and the cost-aware logical framework.
The proofs use Synthetic Tait Computability in the Istari prover, a Martin-Lof style computational type theory.
A Rocq (Coq) mechanization of a semantic logical relation for intuitionistic linear logic session types.
TILLST Type-checker
A type checker for the Timed Intuitionistic Linear Logic Session Type (TILLST) language.
Approved by the POPL 2025 Artifact Evaluation Committee.
SINTEGRITY
An IFC type checker supporting security-polymorphic definitions and regrading policies.
Approved by the ECOOP 2024 Artifact Evaluation Committee.
Publications
and
Preprints
Programming Languages and Type Theories
Stephanie Balzer, Farzaneh Derakhshan, Robert Harper, and Yue Yao. 2023. Logical Relations for Session-Typed Concurrency. CoRR. 2309.00192. Available at https://arxiv.org/abs/2309.00192. To appear in ESOP 2026.
Runming Li, Yue Yao, and Robert Harper. 2026. Mechanizing Synthetic Tait Computability in Istari. In Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs. To appear
Yue Yao, Grant Iraci, Cheng-En Chuang, Stephanie Balzer, and Lukasz Ziarek. 2025. Semantic Logical Relations for Timed Message-Passing Protocols. In Proc. ACM Program. Lang. (POPL)
Tarakaram Gollamudi, Jules Jacobs, Yue Yao, and Stephanie Balzer. 2025. A Semantic Logical Relation for Termination of Intuitionistic Linear Logic Session Types. In 11th International Workshop on Coq for Programming Languages (CoqPL)
Tesla Zhang, Asher Kornfeld, Rui Li, Sonya Simkin, Yue Yao, and Stephanie Balzer. 2025. Mechanizing a Proof-Relevant Logical Relation for Timed Message-Passing Protocols. CoRR. 2511.19521. Available at https://arxiv.org/abs/2511.19521
Tesla Zhang, Sonya Simkin, Rui Li, Yue Yao, and Stephanie Balzer. 2025. A Language-Agnostic Logical Relation for Message-Passing Protocols. CoRR. 2506.10026. Available at https://arxiv.org/abs/2506.10026
Farzaneh Derakhshan, Stephanie Balzer, and Yue Yao. 2024. Regrading Policies for Flexible Information Flow Control in Session-Typed Concurrency. In 38th European Conference on Object-Oriented Programming (ECOOP 2024)
Yue Yao. 2019. Work-Efficient Schedulers. Master's thesis. Carnegie Mellon University
Approximate Logic Synthesis
Chang Meng, Zhuangzhuang Zhou, Yue Yao, Shuyang Huang, Yuhang Chen, and Weikang Qian. 2023. HEDALS: Highly Efficient Delay-Driven Approximate Logic Synthesis. In IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (11)
Zhuangzhuang Zhou, Yue Yao, Shuyang Huang, Sanbao Su, Chang Meng, and Weikang Qian. 2018. DALS: Delay-driven Approximate Logic Synthesis. In 2018 IEEE/ACM International Conference on Computer-Aided Design (ICCAD)
Yue Yao, Shuyang Huang, Chen Wang, Yi Wu, and Weikang Qian. 2017. Approximate Disjoint Bi-Decomposition and Its Application to Approximate Logic Synthesis. In 2017 IEEE International Conference on Computer Design (ICCD)
Services
- Co-reviewed for Symposium on Principles of Programming Languages (POPL 2026).
- Served on the POPL 2026 Artifact Evaluation Commitee.