Curriculum Vitae
Andrew K. Hirsch
http://www.cs.cornell.edu/~akhirsch
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
Theses and 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.
- Semantics for Authorization Logics
Authorization logics are used to describe and prove properties of authorization policies. We give a new semantics for authorization logics, based on the informal notion of semantics for the Nexus Authorization Logic (NAL). We show that this semantics is equivalent to the more traditional Kripke semantics. This work was published in Computer and Communications Security 2013 in Berlin, Germany.
- Domain Specific Language for Composite
Composite is a component-based operating system developed at The George Washington University. I developed a domain specific language for specifing communication between components. The language automatically inserted dynamic checks to ensure that communication happened correctly. This served as my Capstone Design project for my Bachelor’s of Science degree.
- Turing Categories for Computability Theorists
Turing categories are a definition of computability in category theory. I discuss Turing categories, and note their use in proving theories in computability theory. This served as an Honor’s thesis for my Bachelor’s of Science degree.
Teaching Experience
- 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
Strict and Lazy Semantics for Effects, ACM International Conference on Functional Programming, 2018
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
- Computer Science Graduate Organization President, 2015 – 2016
- Theory of Programming Languages Seminar Czar, 2014 – Present
- 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)