About Me

I am a PhD student working on AI viewed as differentiable programming through the lense of programming language techniques. This encompasses both applying program analysis techniques to analyze existing learning systems, and using these techniques as components of new learning systems. Recently, this has meant working on important problems in AI safety such as protecting against adversarial attacks in neural networks. Historically, I’ve done research on metaprogramming using first class type inference, substructural logics, computational geometry for fluid simulations, and computer graphics.


  • Differentiable Abstract Interpretation for Provably Robust Neural Networks Matthew Mirman, Timon Gehr, Martin Vechev, ICML 2018

  • Training Neural Machines with Trace-Based Supervision Matthew Mirman, Dimitar Dimitrov, Pavle Djordjevich, Timon Gehr, Martin Vechev, ICML 2018

  • AI2: Abstract Interpretation of Neural Networks
    Timon Gehr, Matthew Mirman, Dana Drachsler Cohen, Petar Tsankov, Swarat Chaudhuri, Martin Vechev, IEEE S&P 2018

  • Inversion of Quadratic Bezier Triangles
    Gary L. Miller, Matthew Mirman, Todd Phillips
    Fall Workshop in Computational Geometry 2010 - Poster

  • Google Scholar Page



  • Caledon: A higher order meta-programming logic language typed by a pure type system with an infinite universe heirarchy and first class type inference.

  • Forward-Chan: An implementation of a more general “forward” primitive used in the identity rule for the proof terms of the sequent calculus formulation of linear logic, based on traditional channel primitives and mutation.

  • ImperativeHaskell: Proof that haskell can look and act like an imperative language, with a diverse set of imperative primitives

  • RPC-framework: An RPC library for haskell that makes construction of anonymous services both well typed and easy to use, with a modal typed seperating worlds api. Only works with older GHC versions.

  • Conpig: An alternative green threading library for python that automates more of the concurrency.

  • Raskell: linear and ordered typed tagless DSLs.

Contact me

Personal Facts

  • I am a US citizen currently living in Zurich, Switzerland
  • I have also lived in Brooklyn NY, San Francisco CA, Pittsburgh PA, Waltham MA.
  • I am originally from NYC.
  • My accent is not as bad as Feynman’s was.
  • I ride a mountain unicycle.