Seminar for foundations of mathematics and theoretical computer science Faculty of mathematics and physics University of Ljubljana October 15, 2020 Frex - indexing modulo equations with free extensions Ohad Kammar (University of Edinburgh) (joint work with Guillaume Allais, Edwin Brady, and Jeremy Yallop) Abstract: I'll report about ongoing work on an extensible dependently-typed library of algebraic solvers for common algebraic structures based on free extensions (frex): the coproduct of an algebra with a free algebra. One challenge arising when programming with types indexed by values involves convincing the type-checker that two open terms are equal, as variables appearing in open terms get in the way of standard normalisation procedures like beta-reduction. Here I'll focus on indexing by terms malleable to equational reasoning. When the indexing type is the carrier for an algebraic structure, we hypothesise that type-checking modulo this theory amounts to representing the free extension of the algebra structure of this type with a finite set of variables. We propose a library involving two tiers: a user-facing tier for indexing types with algebraic values (‘frexlets'), and a library-developer-facing tier for extending the library to support new algebraic theories (‘core frex'). I'll report and demonstrate our implementation in Brady's upcoming Idris2 programming language.