I am Andrew K. Hirsch, a Postdoctoral Researcher at the Max Planck Institute for Software Systems in Saarbrücken, Germany. I work with Deepak Garg in the Foundations of Computer Security group on applying programming-language theory to computer security.
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.
I’m on the job market for the 2021/2022 season! You can view my job-application materials here.
My Work at a Glance
Research
My research involves applying methods from the theory of programming languages and mathematical logic to computer security. I’m especially focused on 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
I have acted as a teaching assistant in several courses, both at Cornell and at George Washington. I have helped develop several of these courses, including the Programming Languages course at George Washington and a unit on Coq for the Functional Programming course at Cornell.
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.
Research Areas
Information-Flow Control
- 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 Submission
Papers By Date
- Pirouette: Higher-Order Typed Functional Choreographies
With Deepak Garg
To Appear 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 