Ohad Kammar: Frex: indexing modulo equations with free extensions

Datum objave: 9. 10. 2020
Seminar za temelje matematike in teoretično računalništvo
Četrtek, 15. 10. 2020, od 10h do 12h, spletni seminar

Zoom ID 989 0478 8985

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.