Software Engineer


I’m Mauro, a programmer who specializes in static analysis and functional programming. My fascination includes type systems, formal semantics, compilers, software testing and software verification. It is my belief that we can build better software in the long-term by investing in strong static guarantees.

I have worked on a the symbolic execution engine of a program verifier, stress-tested SMT solvers by generating random formulas with known satisfiability and contributed to various open source projects including the OCaml compiler, OCaml preprocessor extensions, the Babel JavaScript transpiler and the Haskell bindings for the Z3 SMT solver.


mnd: A small library for programming with monads in OCaml.


lambda-calculus: A small subset of Haskell translated into and interpreted as Lambda Calculus (LC), implemented in Haskell. My curiosity for this project came during a lecture when the professor said “We will implement Haskell in Haskell” but then only presented an LC interpreter in Haskell. Although LC is only the theoretical base and Haskell implementations use other techniques, I still wanted to see an actual Haskell interpreter based on LC. This allows construction of an LC term which implements LC itself, using the standard Church encoding for most things.


IagoAbal/haskell-z3#61: A user of the library reported non-deterministic segfaults which I investigated. It took me quite a while to figure out what was going on, discussing back and forth with other developers on the issue tracker. Finally we understood the root issue and I introduced locking on the Haskell level to avoid race conditions when calling not-thread-safe C API’s of Z3.

ppx_deriving_yaml#37: This is an OCaml preprocessor library which generates of_yaml and to_yaml functions for a given OCaml type. For a record field, the user can supply a default value which was previously ignored in the to_yaml function. As suggested by a user, I changed the generated implementation to omit default values from the output yaml.