Software

I’m actively developing and contributing to:

• Cubical Agda - A version of Agda with cubical primitives making it into a full-blown proof assistant with support computational univalence and user defined higher inductive types.

• UniMath - A Coq library for formalizing mathematics using the univalent point of view.

I have previously developed:

• cubicaltt - A Haskell implementation of a type theory based on a constructive model in cubical sets. This system provides a computational interpretation to notions from Univalent Foundations and Homotopy Type Theory, most notably the univalence axiom. This has now been succeeded by Cubical Agda.

• yacctt - yet another cartesian cubical type theory. This is a version of cubicaltt based on Cartesian Cubical Type Theory. This has been succeeded by redtt.

• cubical - A predecessor of cubicaltt.

• The Coq Effective Algebra Library (CoqEAL) - A library for conveniently combining proving and efficient computations in the Coq proof assistant.