Researcher in formal methods of mathematics, type theory, category theory, and homotopy theory. Avid user of GNU Guix, Scheme, OCaml, Standard ML, Coq, Haskell, and more! Interested in PRL systems, HOL, and other theorem provers. Lover of software freedom.
Founding member of Symode Engineering.
Reject proprietary, embrace freedom!
GNU.ORG | FSF.ORG