Write a Blog >>
ICFP 2020
Thu 20 - Fri 28 August 2020
Sun 23 Aug 2020 13:00 - 13:30 at TyDe - Session 2

We 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 we 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’). We report and demonstrate our implementation in Brady’s upcoming Idris2 programming language.

Sun 23 Aug

Displayed time zone: Eastern Time (US & Canada) change

12:30 - 14:00
Session 2TyDe at TyDe
Graded Modal Dependent Type Theory (Extended Abstract)
Benjamin Moon School of Computing, University of Kent, Harley D. Eades III Augusta University, Dominic Orchard University of Kent, UK
File Attached
Frex: indexing modulo equations with free extensions (Extended Abstract)
Guillaume Allais University of St Andrews, Edwin Brady University of St. Andrews, UK, Ohad Kammar University of Edinburgh, Jeremy Yallop University of Cambridge
Retrofitting Symbolic Holes to LLVM IR (Extended Abstract)
Bruce Collie University of Edinburgh, Michael F. P. O'Boyle University of Edinburgh