Revising Agda's module system

Jesper Cockx

Date: Wed, June 10, 2020
Time: 12:00
Room: Eelco's Zoom Room

In the 13 years since the original release of Agda 2, the module system designed by Ulf Norell has proven itself to be powerful and robust for many applications. However, two pain points in the current implementation are the printing of names coming from imported modules, and the efficiency issues (e.g. arising from the need to copy modules on application.

In this talk, I will show al alternative presentation of the original design of Agda’s module system, and propose some changes that would hopefully solve the issues with the current implementation. I am especially interested in feedback on further possible improvements to the design.

Previous: Bohdan Liesnikov |
Next: Michael D. Adams |