Frex: programming with equations

Frex offers a new approach to algebraic optimization based on free extensions from universal algebra. Frex provides a common interface to algebraic code, supporting the construction of computations from variables and operations, then automatically optimizing those computations using the corresponding equations.

Frex also offers a new approach to synthesising algebraic proofs in dependently-typed programming languages, extending built-in syntactic equalities to support user-defined equations.

Join the Frex project

Informal enquiries from potential PhD and MPhil students are welcome: contact Ohad Kammar at Edinburgh or Jeremy Yallop at Cambridge.

Papers & extended abstracts