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.
Informal enquiries from potential PhD and MPhil students are welcome: contact Ohad Kammar at Edinburgh or Jeremy Yallop at Cambridge.
Frex: dependently-typed algebraic simplification (pdf, arXiv)
Draft
Guillaume Allais, Edwin Brady, Nathan Corbyn, Ohad Kammar and Jeremy Yallop
Modular construction of multi-sorted free extensions (short paper) (pdf)
PEPM 2023
Guillaume Allais, Nathan Corbyn, Ohad Kammar, Nachiappan Valliappan, Sam Lindley and Jeremy Yallop
Normalization by Evaluation with free extensions (extended abstract) (pdf)
TyDe 2022
Nathan Corbyn, Ohad Kammar, Sam Lindley, Nachiappan Valliappan and Jeremy Yallop
Generalised free extensions (extended abstract) (pdf, poster)
ICFP SRC 2022
Nathan Corbyn
Proof Synthesis with Free Extensions in Intensional Type Theory (pdf)
MEng Dissertation, University of Cambridge (2021)
Nathan Corbyn
Frex: indexing modulo equations with free extensions (extended abstract) (pdf)
TyDe 2020
Guillaume Allais, Edwin Brady, Ohad Kammar and Jeremy Yallop
Partially static data as free extension of algebras (pdf)
ICFP 2018
Jeremy Yallop, Tamara von Glehn and Ohad Kammar
Partially static data as free extension of algebras (short paper) (pdf)
presented at PEPM 2018
Jeremy Yallop, Tamara von Glehn and Ohad Kammar