Curriculum Vitae

Andrew K. Hirsch

Address

113M Davis Hall
University at Buffalo, SUNY
Buffalo, NY 14260

Tel:

+1 (817) 874-2954

PDF Version

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

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

2022

Semantics for Noninterference with Interaction Trees
Lucas Sliver, Paul He, Ethan Cecchetti, Andrew K. Hirsch, and Steve Zdancewic
In Preparation

2022

Logical Relations for Higher-Order Where Declassification
Jan Menz, Andrew K. Hirsch, Peixuan Li, and Deepak Garg
In Preparation

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)