Idris Frex
I contributed to the Idris Frex project, a library which offers a new approach to synthesising algebraic proofs in dependently-typed programming languages, based on free extensions from universal algebra.
My contribution was to extend the library with the construction of the free algebra for the distributive combination of theories, as well as with some additional solvers.
Frex offers a new approach to synthesising algebraic proofs in dependently-typed programming languages, based on free extensions from universal algebra. Frex provides a common interface to algebraic reasoning, supporting the construction of terms from variables and operations, then automatically extending built-in propositional equality to support user-defined equations.