I am an Assistant Research Professor in the Principles of Programming Group of the Computer Science Department at Carnegie Mellon University. I am interested in developing type systems and verification logics for proving correctness and safety of concurrent programs.
Publications
- Logical Relations for Session-Typed Concurrency.
Stephanie Balzer, Farzaneh Derakhshan, Robert Harper, Yue Yao.
CoRR, volume abs/2309.00192, 2023.
[PDF]
[TR]
- DisLog: A Separation Logic for Disentanglement.
Alexandre Moine, Sam Westrick, and Stephanie Balzer.
Under review, 2023.
[PDF]
- Higher-Order Leak and Deadlock Free Locks.
Jules Jacobs and Stephanie Balzer.
Accepted to 50th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2023.
[PDF]
- Recursive Session Logical Relations.
Farzaneh Derakhshan and Stephanie Balzer.
CoRR, volume abs/2208.13741, 2022.
[TR]
- Multiparty GV: Functional Multiparty Session Types With Certified Deadlock Freedom. Jules Jacobs, Stephanie
Balzer, and Robbert Krebbers.
In 27th ACM SIGPLAN International Conference on Functional Programming (ICFP).
Proceedings of the ACM on Programming Languages (PACMPL), volume 6, number ICFP, pages 466-495, 2022.
[PDF]
[Artifact]
- 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.
Distinguished Paper.
[PDF]
[TR]
[Code]
- 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]
- 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]
- Resource-Aware Session Types for Digital Contracts. Ankush Das, Stephanie Balzer,
Jan Hoffmann, Frank Pfenning, and Ishani Santurkar.
In 34th IEEE Computer Security Foundations Symposium (CSF).
Pages 1-16. IEEE 2021
[PDF]
- Manifestly Phased Communication via Shared Session Types.
Chuta Sano, Stephanie Balzer, and Frank Pfenning.
In 23rd International Conference on Coordination Models and Languages (COORDINATION).
Lecture Notes in Computer Science, vol. 12717, pages 23-40.
Springer, 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]
- A Universal Session Type for Untyped Asynchronous Communication. Stephanie Balzer,
Frank Pfenning, and Bernardo Toninho. In 29th International Conference on Concurrency Theory
(CONCUR). Pages 30:1--30:18. LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik,
2018. [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]
- Objects as Session-Typed Processes. Stephanie Balzer and Frank Pfenning. In 5th International Workshop on Programming based on Actors, Agents, and Decentralized Control (AGERE!), affiliated with SPLASH. Pages 13-24. ACM, 2015. [PDF]
- Object Propositions. Ligia Nistor, Jonathan Aldrich, Stephanie Balzer, and Hannes Mehnert. In 19th International Symposium on Formal Methods (FM 2014). Lecture Notes in Computer Science, vol. 8442, pp. 497-513. Springer, 2014. [SpringerLink]
- Wyvern: A Simple, Typed, and Pure Object-Oriented Language. Ligia Nistor, Darya Kurilova, Stephanie Balzer, Benjamin Chung, Alex Potanin, and Jonathan Aldrich. In 5th Workshop on Mechanisms for SPEcialization, Generalization and inHerItance (MASPEGHI), affiliated with ECOOP. Pages 9-16. ACM, 2013. [PDF]
- Selective Ownership: Combining Object and Type Hierarchies for Flexible Sharing. Stephanie Balzer, Thomas R. Gross, and Peter Müller. In 19th International Workshop on Foundations of Object-Oriented Languages (FOOL 2012), affiliated with SPLASH 2012. [PDF]
- Verifying Multi-Object Invariants with Relationships. Stephanie Balzer and Thomas R. Gross. In 25th European Conference on Object-Oriented Programming (ECOOP 2011). Lecture Notes in Computer Science, vol. 6813, pp. 359-383. Springer, 2011. [PDF] [SpringerLink]
- Rumer: a Programming Language and Modular Verification Technique Based on Relationships. Stephanie Balzer. PhD Thesis, ETH Zurich, Nr. 19851, 2011. [PDF] [ETHLink]
- Modular Reasoning about Invariants over Shared State with Interposed Data Members. Stephanie Balzer, Thomas R. Gross. In 4th ACM SIGPLAN Workshop on Programming Languages Meets Program Verification (PLPV 2010), affiliated with POPL 2010, pp. 49-56. ACM, 2010. [PDF] [ACM Portal]
- Objects in Context: An Empirical Study of Object Relationships. Stephanie Balzer, Alexandra Burns, and Thomas R. Gross. Technical Report 594, ETH Zurich (May 2008). [PDF] [ETHLink]
- A Relational Model of Object Collaborations and its Use in Reasoning about Relationships. Stephanie Balzer, Thomas R. Gross, and Patrick Eugster. In 21st European Conference on Object-Oriented Programming (ECOOP 2007). Lecture Notes in Computer Science, vol. 4609, pp. 323-346. Springer, 2007. [PDF] [SpringerLink]
- Member Interposition: How Roles Can Define Class Members. Stephanie Balzer, Thomas R. Gross. In 2nd Workshop on Roles and Relationships in Object Oriented Programming, Multiagent Systems, and Ontologies (Roles 2007), Workshop co-located with ECOOP 2007. Technical Report 2007-9, Technische Universität Berlin (2007).
- Relations for Specifying the Invariant Behavior of Object Collaborations. Stephanie Balzer. In PhD Programme of 9th International Conference on Relational Methods in Computer Science (RelMiCS), 2006.
- Relations: Abstracting Object Collaborations. Stephanie Balzer, Patrick Eugster, and Thomas R. Gross. Technical Report 539, ETH Zurich (November 2006). [PDF] [ETHLink]
- Can Aspects Implement Contracts? Stephanie Balzer, Patrick Th. Eugster, and Bertrand Meyer. In Proceedings of 2nd International Workshop on Rapid Integration of Software Engineering Techniques (RISE), 2005. Lecture Notes in Computer Science, vol. 3943, pp. 145-157. Springer, 2005. [SpringerLink]
- Contracted Persistent Object Programming. Stephanie Balzer. PhD Workshop, ECOOP 2005. [PDF]
- Entwicklung eines metadatengesteuerten Historisierungswerkzeugs für die Aktualisierung von Data Warehouses (Development of a Metadata-driven, History-sensitive Software Component for the Actualization of Data Warehouses). Stephanie Balzer. Master Thesis, University of Zurich, 2001. [PDF]
- Einführung in die objektorientierte Programmierung mit Java (Introduction to Programming in Java). Stephanie Balzer. Semester Thesis, University of Zurich, 1998 (text book for associated lecture). [PDF]
Talks
- Invited speaker at 3rd Joint International Workshop on Linearity and Trends in Linear Logic and its Applications (Linearity \& TLLA) 2022.
- 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.
- Invited speaker at TYPES 2021.
- Invited speaker at Programming Language Approaches to Concurrency- & Communication-cEntric Software (PLACES) 2019.
- 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.
Service
- Program committee member of International Conference on Formal Structures for Computation and Deduction (FSCD) 2024.
- 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).
- Co-organizer of Oregon Programming Languages Summer School (OPLSS) 2023
- Program committee member of OOPSLA 2023.
- Program committee member of ACM SIGPLAN Symposium on Principles of Programming Languages (POPL) 2023.
- Organizing committee member of ECOOP Doctoral Symposium 2022.
- Program committee member of Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP) 2022.
- Program committee member of 28th International Conference on Types for Proofs and Programs (TYPES) 2022.
- Program committee member of International Conference on Functional Programming (ICFP) 2021.
- Program committee member of European Symposium on Programming (ESOP) 2021.
- Organizing committee member of POPL Programming Languages Mentoring Workshop (PLMW) POPL 2021.
- Program committee member of Combined 27th International Workshop on Expressiveness in Concurrency and 17th Workshop on Structural Operational Semantics (EXPRESS/SOS) 2020.
- Program committee member of Conference on Coordination Models and Languages (COORDINATION) 2020.
- Program committee member of Mathematically Structured Functional Programming (MSFP) 2020.
- Member of extended program committee of International Conference on Functional Programming (ICFP) 2020.
- Organizing committee member of Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES) 2020.
- Organizing committee member of POPL Programming Languages Mentoring Workshop (PLMW) POPL 2020.
- Program committee member of Recent Advances in Concurrency and Logic (RADICAL) 2019.
- Program committee member of Trends in Functional Programming (TFP) 2019.
- Invited panelist and mentor at ETAPS 2019 Mentoring Workshop (EMW).
- Program committee member of European Symposium on Programming (ESOP) 2019.
- Program committee member of Conference on Coordination Models and Languages (COORDINATION) 2019.
- Invited panelist at POPL Programming Languages Mentoring Workshop (PLMW) 2019.
- Program committee member of Workshop on Behavioral Types (BEAT) 2019.
- Program committee member of Higher-Order Programming with Effects (HOPE) 2018.
- Committee member of CAV 2017 Artifact Evaluation.
- Committee member of POPL 2016 Artifact Evaluation.
- Program committee member of European Conference on Object-Oriented Programming (ECOOP) 2015.
- Organizing chair of International Workshop of Aliasing, Capabilities, and Ownership (IWACO'14), a workshop co-located with ECOOP 2014.
- Workshop chair of SPLASH 2014.
- Program committee member of Software Engineering Ideen at SE 2014: Konferenz für Software Engineering 2014.
- Workshop chair of SPLASH 2013.
- Organizing chair of Relationships and Associations in Object-Oriented Languages (RAOOL'09), a workshop co-located with ECOOP 2009.
- Member of the organizing committee of Relationships and Associations in Object-Oriented Languages (RAOOL'08), a workshop co-located with OOPSLA 2008.
- Member of the organizing committee of the ECOOP 2006 Doctoral Symposium and PhD Students Workshop.
Supervision
Current Students and Postdoctoral Fellows
- Yue Yao (PhD Student)
- Tarakaram Gollamudi (Postdoctoral Fellow)
Former Students and Postdoctoral Fellows
- Jules Jacobs (PhD Student at Radboud University Nijmegen, co-supervision with Robbert Krebbers, now Postdoctoral Fellow at Cornell)
- Farzaneh Derakhshan (Postdoctoral Fellow, now Assistant Professor at ITT)
Thesis Committee Member
- David Kahn (PhD Dissertation Committee). TBD. CMU
- Klaas Pruiksma (PhD Dissertation Committee). TBD. CMU
- Koen Jacobs (PhD Dissertation Committee). November 2022. KU Leuven
- Farzaneh Derakhshan (PhD Dissertation Committee). May 2021. CMU
M.S. and Research Projects
- Yuanchu Xie (Undergraduate Research Project). Spring 2020. CMU
- Simin Chen (REU Summer Project). Summer, 2012. CMU (with Jonathan Aldrich).
- Reto Conconi (Master Thesis). Fall, 2010. ETH Zurich (with Thomas R. Gross).
- Agnes Sebestyen-Pal (Diploma Thesis). Spring, 2009. ETH Zurich (with Thomas R. Gross).
- Michelle Volery (Master Thesis). Spring, 2009. ETH Zurich (with Thomas R. Gross).
- Andrea Zimmermann (Master Thesis). Fall, 2008. ETH Zurich (with Thomas R. Gross).
- Roland Schilter (Semester Thesis). Spring, 2008. ETH Zurich (with Thomas R. Gross).
- Christoph Bäni (Semester Thesis). Fall, 2007. ETH Zurich (with Thomas R. Gross).
- Alexandra Burns (Master Thesis). Summer, 2006. ETH Zurich (with Thomas R. Gross).
- Alexandra Burns (Semester Thesis). Winter, 2005/2006. ETH Zurich (with Thomas R. Gross).
- Shinji Takasaka (Master Thesis). Summer, 2005. ETH Zurich (with Bertrand Meyer).
Collaborators
- Soares Chen and Bernardo Toninho: Ferrite.
- Ankush Das and Jan Hoffmann and Frank Pfenning: Nomos.
- Marco Peressotti and Fabrizio Montesi: π-calculus and session types.
- Sam Westrick and Umut Acar: type systems for parallelism.
- Henry DeYoung: asynchronous message passing.
- Jon Sterling and Robert Harper: noninterference through the lens of substructural session types and topos theory.
Teaching
- 15-312: Principles of Programming Languages.
- 15-122: Principles of Imperative Programming.
- 15-110: Principles of Computing.
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.