About Me

Dr. Matthew Mirman is a computer scientist, who attained his PhD at ETH Zürich, supervised by Martin Vechev. His main research interests sit at the intersection of programming languages, machine learning, and theory with applications to creating safe and reliable artificial intelligence systems. Prior to ETH, he completed his B.Sc. and M.Sc. at Carnegie-Mellon University supervised by Frank Pfenning.

Publications

• Robustness Certification with Generative Models Matthew Mirman, Alexander Hägele, Timon Gehr, Pavol Bielik, Martin Vechev PLDI 2021

• Universal Approximation with Certified Networks Maximilian Baader, Matthew Mirman, Martin Vechev, ICLR 2020

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

• Fast and Effective Robustness Certification Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, Martin Vechev NeurIPS 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

• More on Google Scholar Page

Education

• ETH Zurich, Secure, Reliable and Intelligent Systems Lab, January 2017 – Current PhD in Computer Science
  Advisor: Martin Vechev

• Carnegie Mellon University, SCS, August 2012 – May 2014
  MSCS in Computer Science
  Thesis: Logic Programming and Type Inference with the Calculus of Constructions
  Advisor: Frank Pfenning

• Carnegie Mellon University, SCS, August 2009 – May 2012
  BS in Computer Science, with University Honors
  College Honors Thesis: Modes for Non Strict Functional Logic Languages
  Advisor: Frank Pfenning

• Carnegie Mellon University, MCS, August 2009 – May 2012
  BS in Mathematical Sciences, with University Honors

Projects

• DiffAI: Differentiable Abstract Interpretation for Robustness

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

• MentisOculi: Differentiable pathtracing

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

• PySearch: Python Function Search by Description.

Contact me

• matt@mirman.com
• matthew.mirman@inf.ethz.ch
• Office: CNB H 100.5

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.