I'm a Senior Principal Applied Scientist in the Automated Reasoning Group at AWS. I'm also the Chief Architect and co-founder of the Lean FRO, a non-profit organization dedicated to the development of the Lean theorem prover and programming language.

Projects

Lean Theorem Prover

Previous Projects

Z3 SMT Solver

Yices 1.0 SMT Solver

SAL (the Symbolic Analysis Laboratory)

Teaching

Here is a list of courses I have taught in the past.

• Tools and Algorithms in Real Algebraic Geometry, University of Milan, Italy, May 2013.
• Decision Methods for Arithmetic, Third Summer School on Formal Techniques, Menlo Park, 2013, (part 1, part 2, part 3, exercises).
• Second Summer School on Formal Techniques, Menlo Park, 2012.
• First Summer School on Formal Techniques, Menlo Park, 2011.
• Satisfiability Modulo Theories (SMT): Ideas & Applications, Universita Degli Studi di Milano, Italy, March 2010 (part 1, part 2, part 3, part 4, assignment).
• On Designing and Implementing Satisfiability Modulo Theory Solvers, Summer School 2009: Verification Technology, Systems & Applications, Nancy, France (lecture 1, lecture 2).
• SMT Solvers: Theory and Implementation, Summer School on Logic and Theorem Proving in Programming Languages, Oregon 2008 (exercises).
• CS359: Little Engines of Proof, Stanford University, Fall 2003.