Curriculum Vitae
Andrew K. Hirsch
http://people.mpi-sws.org/~akhirsch
Education
- PhD in Computer Science, Cornell University, 2019
- Master of Science in Computer Science, Cornell University, 2016
- Bachelors of Science in Computer Science and Pure Mathematics, The George Washington University, 2013
Research Interests
- Programming Languages
- Mathematical Logic and Foundations of Mathematics
- Category Theory
- Foundations of Computer Security
Research Projects
- Flow-Limited Authorization Logics
Authorization logics are often used to describe correctness for authorizaiton mechanisms in distributed systems. They allow flexibility in defining authorization policies and proof-theoretic tools for providing security guarantees. However, these logics generally do not reflect the fact that often authorization decisions are based on private or low-integrity data. We (Hirsch, Cecchetti, Arden, and Tate) are developing FLAFOL, the Flow-Limited Authorization First-Order Logic, which is an authorization logic with information flow labels. FLAFOL describes the correctness of authorization mechanisms which respect information flow policies. FLAFOL also provides unique security guarantees: not only do the standard notions of non-interference for authorization logic and information flow labels hold, but we can show that the action of a correct authorization mechanism (with reference to FLAFOL) cannot leak private information, as determined by the labels.
- Categorical Semantics for Type-And-Effect Systems
Effects are ubiquitous in programming languages. Ever since Moggi introduced monads in his computational lambda calculus, there have been generalizations and reformulations of categorical semantics of effect systems. My work involves pushing back on the assumptions that are made in these models, and in applying those models to understand issues in programming languages. My most recent work involves relaxing the assumptions about the structure of the language that these models are built on.
Teaching Experience
- Advanced Programming Languages, Spring 2019
Graduate Teaching Assistant, Cornell University
- Category Theory for Computer Scientists, Spring 2018
Part-Time Graduate Teaching Assistant, Cornell University
- Functional Programming and Data Structures, Fall 2017
Graduate Teaching Assistant, Cornell University
- Programming Languages, Fall 2016
Graduate Teaching Assistant, Cornell University
- Computer System Organization and Programming, Spring 2014
Graduate Teaching Assistant, Cornell University
- Database Systems, Fall 2013
Graduate Teaching Assistant, Cornell University
- Principals of Programming Languages, Spring 2013
Undergraduate Teaching Assistant, The George Washington University
- Introduction to Mathematical Reasoning, Fall 2012
Undergraduate Teaching Assistant, The George Washington University
Current Position
Postdoctoral Researcher in Computer Security Foundations, Max Planck Institute for Software Systems
Past Positions
- Intern, GrammaTech, 2016
- Research on the BRASS project
- Apply type-theoretic and programming-languages ideas to software engineering research
- Development in Common Lisp
- Student Researcher, GWU Department of Computer Science, 2012
- Work on semantics for authorization logics
- Undergraduate Teaching Assistant, GWU Department of Mathematics, 2013
- Assist students in learning how to write proofs
- Contractor, Omnipacs, 2011 – 2012
- PHP and Javascript web development
- MySQL, PostgresSQL, and couchDB database administration
- Java applet development
- Student Technician, Student Technical Services, GWU, 2009 – 2011
- Assisted students in connecting to the network
- Answered technical questions for students
- Did laptop repairs on Dell and Apple laptops
Writing and Talks
First-Order Logic for Flow-Limited Authorizat, IEEE Symposium on Computer Security Foundations, 2020
First-Order Logic for Flow-Limited Authorization, Talk given at Foundations of Computer Security Workshop (Unpublished), 2019 http://homepages.cs.ncl.ac.uk/charles.morisset/fcs2019
Strict and Lazy Semantics for Effects, ACM International Conference on Functional Programming, 2018 https://dl.acm.org/citation.cfm?doid=3243631.3236783 http://www.cs.cornell.edu/~akhirsch/pubs/strict_and_lazy_semantics_for_effects.html
Belief Semantics for Authorization Logic, ACM Conference on Computer and Communications Security, 2013 https://dl.acm.org/citation.cfm?id=2516667
Nexus Authorization Logic (NAL): Logical Results, Technical Report, 2012 http://arxiv.org/abs/1211.3700
Mechanized Metatheory for Authorization Logic, Talk given at NJPLS, 2012
Service
- POPL PLMW Panelist, 2020
- POPL Artifact Evaluation Committee, 2020
- Eastern Great Lakes Programming Languages and Systems Symposium Chair, 2019
- Theory of Programming Languages Seminar Czar, 2014 – 2018
- Computer Science Graduate Organization President, 2015 – 2016
- Programming Languages Discussion Group Czar, 2013 – 2015
- Belle Sherman Elementary After School Program Volunter, 2014
- President, GWU ACM, 2011 – 2013
- Coach, GWU ACM ICPC Team, 2012
- Treasurer, GWU ACM, 2010
- Team Member, GWU ACM ICPC Team, 2009 – 2011
Selected Relevant Courses
- Category Theory for Computer Scientists (Fall 2014)
- Advanced Programming Languages (Spring 2014)
- Programming Languages (Spring 2010)
- Computability Theory (Spring 2011)
- Cryptography (Spring 2011)
- Topics in Logic – Algorithmic Learning Theory (Fall 2011)
- Independent Study – Category Theory (Spring 2012)
- Topics in Security – The Science of Security (Spring 2012)
- Mathematical Logic (Fall 2012)
- Topics in Logic – Computability and Logic (Fall 2012 – Spring 2013)