I am Andrew K. Hirsch, an Assistant Professor in the Department of Computer Science and Engineering at the University at Buffalo, SUNY. My research is on programming languages for decentralized systems. My focus is on choreographic programming, a programming paradigm for message-passing concurrency. I also work on information-flow security, and on other, related, ideas. I’m currently recruiting students. If you’re interested in working with me, please send me an email!
Before I came to Buffalo, I was a postdoc at the Max Planck Institute for Software Systems (MPI-SWS) in Saarbrücken, Germany. I worked with Deepak Garg in the Foundations of Security group. I earned my Ph.D. in 2019 from Cornell University in Ithaca, NY, USA. There, I worked with Ross Tate on programming-language foundations, focusing on the theory of computational effects. Before that, I attended The George Washington University in Washington, DC, where I earned a Bachelor’s of Science degree in Computer Science and Pure Mathematics.
My Work at a Glance
Research
My research involves applying methods from the theory of programming languages and mathematical logic to concurrency and computer security. I’m especially focused on choreographies, static information-flow control, and authorization logic. I’m also interested in the theory of effects more broadly, especially reasoning about effects in lazy programming.
Teaching
In the fall, I’m teaching CSE 505: Foundations of Programming Languages.
Service
In my role as a computer scientist, I have acted in service to both my research community and my local community. On the research side, I have acted as a reviewer and have organized several meetings, including a regional meeting which attracted researchers from Cornell, Rochester Institute of Technology, Carnegie Mellon, and more.
Locally, I worked with the Ithaca School District to teach mathematics and computer science in elementary schools, giving young students a positive experience with both.
Students
- Frank (Feng-Mao) Tsai
PhD, University at Buffalo
Website: https://frankt716.github.io/
Research Areas
Information-Flow Control
- Semantics for Noninterference with Interaction Trees
Lucas Silver, Paul He, Ethan Cecchetti, Andrew K. Hirsch, and Steve Zdancewic
To Appear in ECOOP 2023 - Compositional Security Definitions for Higher-Order Where Declassification
Jan Menz, Andrew K. Hirsch, and Deepak Garg
To Appear in OOPSLA 2023 - Giving Semantics to Program-Counter Labels via Secure Effects
Andrew K. Hirsch and Ethan Cecchetti
In POPL 2021 - First-Order Logic for Flow-Limited Authorization
Andrew K. Hirsch, Pedro H. Azevedo de Amorim, Ethan Cecchetti, Ross Tate, and Owen Arden
In CSF 2020
Computational Effects
- Giving Semantics to Program-Counter Labels via Secure Effects
With Ethan Cecchetti
In POPL 2021 - Strict and Lazy Semantics for Effects
With Ross Tate
In ICFP 2018
Authorization Logic
- First-Order Logic for Flow-Limited Authorization
With Pedro H. Azevedo de Amorim, Ethan Cecchetti, Ross Tate, and Owen Arden
In CSF 2020 - Belief Semantics of Authorization Logic
With Michael Clarkson
In CCS 2013
Choreographic Programming
- Pirouette: Higher-Order Typed Functional Choreographies
With Deepak Garg
In POPL 2022
Papers By Date
- Semantics for Noninterference with Interaction Trees
Lucas Silver, Paul He, Ethan Cecchetti, Andrew K. Hirsch, and Steve Zdancewic
To Appear in ECOOP 2023 - Compositional Security Definitions for Higher-Order Where Declassification
Jan Menz, Andrew K. Hirsch, and Deepak Garg
To Appear in OOPSLA 2023 - Pirouette: Higher-Order Typed Functional Choreographies
With Deepak Garg
In POPL 2022 - Giving Semantics to Program-Counter Labels via Secure Effects
With Ethan Cecchetti
In POPL 2021 - First-Order Logic for Flow-Limited Authorization
Andrew K. Hirsch, Pedro H. Azevedo de Amorim, Ethan Cecchetti, Ross Tate, and Owen Arden
In CSF 2020 - Strict and Lazy Semantics for Effects
Andrew K. Hirsch and Ross Tate
In ICFP 2018 - Belief Semantics of Authorization Logic
Andrew K. Hirsch and Michael Clarkson
In CCS 2013
Andrew K. Hirsch 