Revising Agda's module system

Jesper Cockx

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. https://github.com/agda/agda/issues/4331) 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 | Writing plugins and proving them correct in MetaCoq
Next: Michael D. Adams | Language Techniques that Enable Higher-levels of Abstraction in Programming