I am an Assistant Professor in the Principles of Programming Group of the Computer Science Department at Carnegie Mellon University.
The goal of my research is to enable the construction of failure-free software, software that is correct by construction and secure to run. In pursuit of this goal, I am deploying rigorous reasoning methods, such as type systems and verification logics, which allow statement of the desired properties and a formal proof of their adherence. To ensure scalability, I use compositional methods, guaranteeing that individually verified parts compose to a verifiable whole. To ensure practicality, I consider verification needs arising from real-world problems. Tangible results of my research include not only formal models with correctness proofs but also software artifacts.
I received my PhD from ETH Zurich. My advisor was Thomas R. Gross.
Latest news
| February, 2026 | My collaborators and I are honored to receive an ETAPS 2026 Distinguished Paper award. |
| December, 2025 | Our paper on Recursive Logical Relations for Intuitionistic Linear Logic Session Types has been accepted to the 35th European Symposium on Programming (ESOP). |
| December, 2025 | Sonya Simkin has successfully defended her Master's thesis entitled Logical Relations for Noninterference with Cryptography. |
Selected publications
- Recursive Logical Relations for Intuitionistic Linear Logic Session Types. Stephanie Balzer, Farzaneh Derakshan, Robert Harper, and Yue Yao. Accepted to 35th European Symposium on Programming (ESOP). 2026.
- TypeDis: A Type System for Disentanglement. Alexandre Moine, Stephanie Balzer, Alex Xu, and Sam Westrick. In 53rd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). Proceedings of the ACM on Programming Languages (PACMPL), volume 10, number POPL, pages 354-383, 2026. [PDF] [TR] [Artifact]
- Semantic Logical Relations for Timed Message-Passing Protocols. Yue Yao, Grant Iraci, Cheng-En Chuang, Stephanie Balzer, and Lukasz Ziarek. In 52nd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). Proceedings of the ACM on Programming Languages (PACMPL), volume 9, number POPL, pages 1750-1781, 2025. [PDF] [TR] [Artifact]
- Regrading Policies for Flexible Information Flow Control in Session-Typed Concurrency. Farzaneh Derakhshan, Stephanie Balzer, and Yue Yao. In 38th European Conference on Object-Oriented Programming (ECOOP). LIPIcs, volume 313, pages 11:1-11:29, 2024. [PDF] [TR] [Artifact]
- Information Flow Control in Cyclic Process Networks. Bas van den Heuvel, Farzaneh Derakhshan, and Stephanie Balzer. In 38th European Conference on Object-Oriented Programming (ECOOP). LIPIcs, volume 313, pages 40:1-40:30, 2024. [PDF] [TR]
- DisLog: A Separation Logic for Disentanglement. Alexandre Moine, Sam Westrick, and Stephanie Balzer. In 51th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). Proceedings of the ACM on Programming Languages (PACMPL), volume 8, number POPL, pages 302-331, 2024. [PDF] [Artifact]
- Logical Relations for Session-Typed Concurrency. Stephanie Balzer, Farzaneh Derakhshan, Robert Harper, Yue Yao. CoRR, volume abs/2309.00192, 2023. [PDF] [TR]
- Higher-Order Leak and Deadlock Free Locks.
Jules Jacobs and Stephanie Balzer.
In 50th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). Proceedings of the
ACM on Programming Languages (PACMPL), volume 7, number POPL, pages 1027-1057, 2023.
[PDF]
[Artifact]
ACM SIGPLAN Distinguished Paper. - Ferrite: A Judgmental Embedding of Session Types in Rust. Soares Chen, Stephanie Balzer, and Bernardo Toninho.
In 36th European Conference on Object-Oriented Programming (ECOOP).
LIPIcs, volume 222, pages 22:1-22:28, 2022.
[PDF]
[TR]
[Code]
ECOOP Distinguished Paper.
- Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation Logic. Jules Jacobs, Stephanie
Balzer, and Robbert Krebbers. In 49th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). Proceedings of the
ACM on Programming Languages (PACMPL), volume 6, number POPL, pages 1-33, 2022. [PDF]
[Artifact]
- Session Logical Relations for Noninterference. Farzaneh Derakhshan, Stephanie
Balzer, and Limin Jia. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS).
Pages 1-14. IEEE 2021.
[PDF]
[TR]
- Manifest Deadlock-Freedom for Shared Session Types. Stephanie Balzer, Bernardo
Toninho, and Frank Pfenning. In 28th European Symposium on Programming (ESOP). Lecture Notes in Computer Science, vol. 11423, pp. 611-639.
Springer, 2019. [PDF]
- Manifest Sharing with Session Types. Stephanie Balzer and Frank Pfenning. In 22nd
ACM SIGPLAN International Conference on Functional Programming (ICFP). Proceedings of the
ACM on Programming Languages (PACMPL), volume 1, number ICFP, pages 37:1-37:29, 2017. [PDF]
For a complete listing, click here or check out my dblp entry.
Selected talks
- Invited speaker on Session Logical Relations for Noninterference at School of Computer and Cyber Sciences (CCS) Colloquium Series at Augusta University. [Video]
- Invited lecturer at Oregon Programming Language Summer School (OPLSS) 2022.
- Invited lecturer at Oregon Programming Language Summer School (OPLSS) 2021.
- Keynote speaker at Typelevel Summit Philadelphia
2019.
Recording: [Video] [Slides] - Tutorial on Session-Typed Concurrent Programming at 46th ACM
SIGPLAN Symposium on Principles of Programming Languages (POPL) 2019.
Slides: [PDF] - Invited lecturer at Oregon Programming Language Summer School (OPLSS) 2018.
Recent and current service
- Program committee member of ACM SIGPLAN International Conference on Functional Programming (ICFP) 2026.
- Program committee member of ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM) 2026.
- Program committee member of ACM SIGPLAN Symposium on Principles of Programming Languages (POPL) 2026.
- Program committee member of ACM/IEEE Symposium on Logic in Computer Science (LICS) 2025.
- Program committee member of International Conference on Foundations of Software Science and Computation Structures (FoSSaCS) 2024.
- Organizing committee member of Dagstuhl Seminar 24051 on Next Generation Protocols for Heterogeneous Systems (January 28 - February 2, 2024).
- Program committee member of OOPSLA 2023.
- Program committee member of ACM SIGPLAN Symposium on Principles of Programming Languages (POPL) 2023.
- Founder of and steering committee member of PL Scholars Network, present.
- Steering committee chair of Programming Languages Mentoring Workshop (PLMW) 2023-2025.
- Co-organizer of Oregon Programming Languages Summer School (OPLSS) 2023.
For a complete listing, click here.
Current Group Members
- Yue Yao (PhD Student)
- Yinsen (Tesla) Zhang (PhD Student)
- Zak Kent (PhD Student, co-advised with Guy Blelloch)
- Sonya Simkin (M.S. Student)
- Rui Li (M.S. Student)
- Tucker Beaudin (M.S. Student)
- Elisenda Lee-Palou (Undergraduate Student)
- Asher Kornfeld-Narotzky (Undergraduate Student)
- Anrui Liu (Undergraduate Student)
For a complete listing, click here.
Collaborators
- Alexandre Moine and Sam Westrick: type systems for disentanglement.
- Henry DeYoung: asynchronous message passing.
- Farzaneh Derakhshan and Robert Harper: logical relations for concurrency.
Teaching
- 15-150: Functional Programming (F24, F25).
- 15-312: Foundations of Programming Languages (S19, S24, S25, S26).
- 15-122: Principles of Imperative Programming (S16).
- 15-110: Principles of Computing (F17).
Research Funding
- NSF CAREER Award on A Semantic Framework for Verifying Heterogeneous Applications, 2025.
- NSF Award on Integrated Verification of IoT and Real-time Communication Protocols, 2022.
- AFOSR Award on Session Types and Phase Distinctions for Noninterference (FA9550-21-1-0385), 2021.
- CyLab Seed Funding on Static Enforcement of Information Flow Policies on Event-driven Programs, 2020.
- NSF Award on Enriching Session Types for Practical Concurrent Programming, 2017.
- Mozilla Research Grant, 2016.