Andrew K. Hirsch
Address
113M Davis Hall
University at Buffalo, SUNY
Buffalo, NY 14260
Research Interest & Objectives
I use ideas from theory of programming languages to explore issues in computer security and concurrency. I am especially interested in giving foundations to information-flow security, authorization, and choreographic programming. By using theoretical tools, I create principled, general mechanisms for enforcing guarantees and proof techniques for verified-correct programs. Moreover, I develop those theoretical tools to give them the necessary power.
Keywords: • Choreographic Programming • Information Security • Authorization • Programming Language Semantics • Program Verification • Mathematical Logic • Foundations of Mathematics
Education
2019
PhD, Cornell University
Computer Science
Thesis: Semantics for Secure Software
Supervisor: Ross Tate
2016
Master of Science, Cornell University
Computer Science
2013
Bachelor of Science, The George Washington University
Computer Science & Mathematics
Professional Appointments
2022-Present
Assistant Professor
Computer Science and Engineering
University at Buffalo, SUNY
Buffalo, NY, USA
2019-2022
Postdoctoral Researcher
Foundations of Computer Security Group
Max Planck Institute for Software Systems
Saarbrücken, Germany
Publications
Peer-Reviewed Conferences
2023
Semantics for Noninterference with Interaction Trees
Lucas Sliver, Paul He, Ethan Cecchetti, Andrew K. Hirsch, and Steve Zdancewic
To Appear in the European Conference on Object-Oriented Programming (ECOOP)
DOI: Forthcoming
2023
Compositional Security Definitions for Higher-Order Where Declassification
Jan Menz, Andrew K. Hirsch, Peixuan Li, and Deepak Garg
To Appear in Object-Oriented Programming, Systems, and Languages (OOPSLA)
DOI: Forthcoming
2022
Pirouette: Higher-Order Typed Functional Choreographies
Andrew K. Hirsch and Deepak Garg
Principles of Programming Languages (POPL)
DOI: 10.1145/3498684
2021
Giving Semantics to Program-Counter Labels via Secure Effects
Andrew K. Hirsch and Ethan Cecchetti
Principles of Programming Languages (POPL)
DOI: 10.1145/3434316
2020
First-Order Logic for Flow-Limited Authorization
Andrew K. Hirsch, Pedro H. Azevedo de Amorim, Ethan Cecchetti, Ross Tate, and Owen Arden
Computer Security Foundations
DOI: 0.1109/CSF49147.2020.00017
2018
Strict and Lazy Semantics for Effects
Andrew K. Hirsch and Ross Tate
Inernational Conference on Functional Programming (ICFP)
DOI: 10.1145/3236783
2013
Belief Semantics for Authorization Logic
Andrew K. Hirsch and Michael R. Clarkson
Computer and Communications Security (CCS)
DOI: 10.1145/2508859.2516667
Workshops with Unpublished Proceedings
2022
Compositional Higher-Order Declassification using Logical Relations
Jan Menz, Andrew K. Hirsch, and Deepak Garg
Foundations of Computer Security (FCS)
2021
Security-Preserving Program Transformations with ITrees
Lucas Silver, Andrew K. Hirsch, Ethan Cecchetti, Paul He, and Steve Zdancewic
Foundations of Computer Security (FCS)
2020
Noninterference Half-Off
Andrew K. Hirsch and Ethan Cecchetti
Foundations of Computer Security (FCS)
2019
First-Order Logic for Flow-Limited Authorization
Andrew K. Hirsch, Pedro H. Azevedo de Amorim, Ethan Cecchetti, Ross Tate, and Owen Arden
Foundations of Computer Security (FCS)
Technical Reports
2020
First-Order Logic for Flow-Limited Authorization
Andrew K. Hirsch, Pedro H. Azevedo de Amorim, Ethan Cecchetti, Ross Tate, and Owen Arden
Max Planck Institute for Software Systems
URL: https://arxiv.org/abs/2001.10630
2012
Nexus Authorization Logic (NAL): Logical Results
Andrew K. Hirsch and Michael R. Clarkson
The George Washington University
URL: https://arxiv.org/abs/1211.3700
2013
Belief Semantics of Authorization Logic
Andrew K. Hirsch and Michael R. Clarkson
The George Washington University
URL: https://arxiv.org/abs/1302.2123
In Submission & In Perparation
2022
Process Polymorphism in Choreographies
Eva Graversen, Andrew K. Hirsch, and Fabrizio Montesi
In Submission to POPL 2023
Invited Talks
2021
Semantic Techniques for Information-Flow Languages
University of California, Berkeley
2021
Semantic Techniques for Information-Flow Languages
Boston University
2021
Concurrent Interpretations of Authorization Logic
Boston Computing Club
2020
Towards Computational Models for Authorization Logic
Aarhus University
2019
First-Order Logic for Flow-Limited Authorization
University of California, Santa Cruz
2017
Usable Models of Effects
University at Buffalo, SUNY
2015
Strictness, Laziness, and Effects
The George Washington University
Service
2023
International Conference on Functional Programming (ICFP)
Program Committee Member
2023
Object-Oriented Systems, Languages, and Applications (OOPSLA)
Extended Review Committee and Artifact Review Committee Member
2023
Programming-Languages Approaches to Concurrency and Communication-cEntered Software (PLACES)
Program Committee Member
2023
Principles of Programming Languages (POPL)
Student Research Competition Committee Member and Judge
2022
Haskell Symposium
Program Committee Member
2021
International Conference on Functional Programming (ICFP)
Student Research Competition Committee Member and Judge
2021
Programming Languages and Analysis for Security (PLAS)
Program Committee Member
2020
Foundations of Computer Security (FCS)
Program Committee Member
2020
Principles of Programming Languages (POPL)
Artifact Evaluation Committee Member
2019
Eastern Great Lakes Programming Languages and Systems (EGLPLS)
Chair
Teaching Experience
Spring 2023
Great Works of Programming Languages (Professor, University at Buffalo)
Fall 2022
Foundations of Programming Languages (Professor, University at Buffalo)
Summer 2022
Category Theory Seminar (Volunteer, Universität des Saarlandes)
Spring 2019
Advanced Programming Languages (Graduate TA, Cornell University)
Spring 2018
Category Theory for Computer Scientists (Graduate TA, Cornell University)
Fall 2017
Functional Programming and Data Structures (Graduate TA, Cornell University)
Fall 2016
Programming Languages (Graduate TA, Cornell University)
Spring 2014
Computer System Organization and Programming (Graduate TA, Cornell University)
Fall 2013
Database Systems (Graduate TA, Cornell University)
Andrew K. Hirsch 