Curriculum Vitae

Andrew K. Hirsch

http://www.cs.cornell.edu/~akhirsch

akhirsch@cs.cornell.edu

Education

• PhD in Computer Science, Cornell University (Expected), 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
• Information and Systems 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

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 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

• 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)