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.
Selected publications
- Regrading Policies for Flexible Information Flow Control in Session-Typed Concurrency. Farzaneh Derakhshan, Stephanie Balzer, and Yue Yao.
To appear in 38th European Conference on Object-Oriented Programming (ECOOP).
2024.
[TR]
- Information Flow Control in Cyclic Process Networks. Bas van den Heuvel, Farzaneh Derakhshan, and Stephanie Balzer.
To appear in 38th European Conference on Object-Oriented Programming (ECOOP).
2024.
[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/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)
- Sonya Simkin (M.S. Student)
- Rui Li (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).
- 15-312: Principles of Programming Languages (S19, S24).
- 15-122: Principles of Imperative Programming (S16).
- 15-110: Principles of Computing (F17).
Research Funding
- 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.