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.

Conference Day
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 MoonSchool of Computing, University of Kent, Harley D. Eades IIIAugusta University, Dominic OrchardUniversity of Kent, UK
File Attached
Frex: indexing modulo equations with free extensions (Extended Abstract)
Guillaume AllaisUniversity of St Andrews, Edwin BradyUniversity of St. Andrews, UK, Ohad KammarUniversity of Edinburgh, Jeremy YallopUniversity of Cambridge
Retrofitting Symbolic Holes to LLVM IR (Extended Abstract)
Bruce CollieUniversity of Edinburgh, Michael F. P. O'BoyleUniversity of Edinburgh