Contracted with IOHK to deliver formal methods and Haskell development work.
Part of a team developing a semi-formal specification for cryptocurrency wallets, along with an implementation of that specification in Haskell.
Principal investigator and architect of a system for injecting custom security policy enforcement into off-the-shelf iOS apps.
Principal investigator and architect of a platform that lowers the barrier-to-entry for binary rewriting and patching of embedded systems.
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.
Designed and developed an automated tool for trend prediction, situational awareness, and family classification of malware.
Worked with a team of developers to create novel methods for exact decompilation of binary code to C.
Developed and implemented a best-in-class algorithm for inferring types and most-general interfaces for machine-code functions.
Designed and implemented a variety of novel static analyses for stripped binary code. Optimized and debugged existing static analysis implementations.
Continued development, testing, and client interactions for an inverse linker, producing object files and headers from compiled binaries.
Created a user-programmable and extensible application (FractalStream) for the investigation of real and complex dynamical systems in one or more variables.
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.
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.
Developed and taught an experimental Calculus I course, using nilpotent infinitesimals.
Developed and taught a freshman writing seminar, "Experiencing Mathematics Through Writing".
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.
Planned and supervised an REU program (Research Experience for Undergraduates) on sub-Riemannian geometries.
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.
▻ Pure and applied mathematics, software development, exposition.
▻ Program analysis, binary analysis, machine learning.
▻ Software design, research and development, project management.
Haskell, C++, Python.
Objective C, machine code (x86, ARM), C, Scheme, Common Lisp, OCaml.
Public speaking, teaching, proposal writing, informal writing.
Clawhammer banjo, baking, Go (AGA 2 dan), sailing (poorly).
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)
Ph.D. Mathematics, Cornell University (2010). Advisor: John Hamal Hubbard
M.A. Mathematics, Cornell University (2006).
B.A. Mathematics, Hampshire College (2003).