Professional history by category

Formal methods development contract with IOHK
Kataskeue LLC, 2018 -- present

Contracted with IOHK to deliver formal methods and Haskell development work.

Semi-formal Haskell development
Input Output HK, 2018 -- present

Part of a team developing a semi-formal specification for cryptocurrency wallets, along with an implementation of that specification in Haskell.

Customizable iOS security policies (PI)
GrammaTech, Inc., 2017 -- 2018

Principal investigator and architect of a system for injecting custom security policy enforcement into off-the-shelf iOS apps.

Simplifying patch development for legacy binaries (PI, Phase I and II)
GrammaTech, Inc., 2016 -- 2018

Principal investigator and architect of a platform that lowers the barrier-to-entry for binary rewriting and patching of embedded systems.

Logical representations of cyber-physical systems
GrammaTech, Inc., 2016 -- 2018

Developed a range of techniques for automatically extracting models of machine-code functions, suitable for interacting with off-the-shelf SMT solvers and model checkers.

Malware trend prediction
GrammaTech, Inc., 2016

Designed and developed an automated tool for trend prediction, situational awareness, and family classification of malware.

Novel decompilation techniques
GrammaTech, Inc., 2015 -- 2016

Worked with a team of developers to create novel methods for exact decompilation of binary code to C.

Type inference for machine code
GrammaTech, Inc., 2014 -- 2015

Developed and implemented a best-in-class algorithm for inferring types and most-general interfaces for machine-code functions.

Static analysis of machine code
GrammaTech, Inc., 2012 -- 2014

Designed and implemented a variety of novel static analyses for stripped binary code. Optimized and debugged existing static analysis implementations.

Un-linking compiled binaries
GrammaTech, Inc., 2012 -- 2013

Continued development, testing, and client interactions for an inverse linker, producing object files and headers from compiled binaries.

FractalStream
Cornell University, 2009

Created a user-programmable and extensible application (FractalStream) for the investigation of real and complex dynamical systems in one or more variables.

Teaching and course development
Mount Holyoke College, 2010 -- 2012

Developed and taught a variety of courses, including Differential Equations, Applied Mathematics, Linear Algebra, Complex Analysis, and the calculus sequence. Developed new teaching material and methodology making use of the SageMath web notebook interface. Developed novel, open-ended assessments for Calculus, Linear Algebra, and Differential Equations.

Instructor
Cornell University, 2005 -- 2008

Developed, taught, and assisted with a variety of courses, including: calculus, discrete mathematics, differentiable manifolds, and a unified Theoretical Linear Algebra and Calculus sequence. Courses of particular note are mentioned below.

Experimental Calculus I course
Cornell University, 2007

Developed and taught an experimental Calculus I course, using nilpotent infinitesimals.

Freshman Writing Seminar
Cornell University, 2008

Developed and taught a freshman writing seminar, "Experiencing Mathematics Through Writing".

Authoring research proposals
GrammaTech, Inc., 2014 -- 2018

Primary or contributing author to six proposals in response to government solicitations, with a win ratio of 66%. Performed as principal investigator on three of the resulting projects.

Research supervisor
Mount Holyoke College, 2012

Planned and supervised an REU program (Research Experience for Undergraduates) on sub-Riemannian geometries.

Research planning and supervision
Cornell University, 2009, 2010

Planned and supervised seven undergraduate summer research projects on a variety of topics, including conjectures on the Schramm-Loewner equation, minimal surfaces, discrete differential geometry, and combinatorics.

Skills

Broadly

▻ Pure and applied mathematics, software development, exposition.

▻ Program analysis, binary analysis, machine learning.

▻ Software design, research and development, project management.

Preferred languages

Haskell, C++, Python.

Other languages

Objective C, machine code (x86, ARM), C, Scheme, Common Lisp, OCaml.

Expository

Public speaking, teaching, proposal writing, informal writing.

Less marketable

Clawhammer banjo, baking, Go (AGA 2 dan), sailing (poorly).

Publications

Ghosts of Departed Proofs (Functional Pearl), in Haskell Symposium 2018 (ICFP). (2018)

Evolving Exact Decompilation, in BAR 2018 (NDSS). (2018)

Polymorphic Type-Inference for Machine Code, in Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '16). (2016)

Polymorphic Type Inference for Machine Code (slides), (2016)

Geometric Bäcklund Transformations in Homogeneous Spaces, doctoral thesis. Cornell University. (2012)

Calculus on Categories, preprint. (2006)

Education

Ph.D. Mathematics, Cornell University (2010). Advisor: John Hamal Hubbard

M.A. Mathematics, Cornell University (2006).

B.A. Mathematics, Hampshire College (2003).