Improving Agda's module system

Improving Agda's module system

de Bruin, Ivar (TU Delft Electrical Engineering, Mathematics and Computer Science; TU Delft Programming Languages)

Cockx, J.G.H. (mentor)
Liesnikov, B. (mentor)
van Deursen, A. (graduation committee)

Delft University of Technology

Computer Science

2023-07-05

Agda is a language used to write computer-verified proofs. It has a module system that provides namespacing, module parameters and module aliases. These parameters and aliases can be used to write shorter and cleaner proofs. However, the current implementation of the module system has several problems, such as an exponential desugaring of module aliases. This thesis shows how the module system can be changed to address these problems. We have found that we do not need any desugarings during type-checking, but can instead handle module parameters and aliases during signature lookup by making a small change to the scope-checker, completely eliminating any exponential growth problems and unnecessary complexity. This will allow users to make more effective use of the module system, simplifying their proofs. Furthermore, the improvements to the module system will allow future research to fix the problems with Agda's implementation of pretty-printing, records and open public statements.

Dependent Types
Agda
type checking

http://resolver.tudelft.nl/uuid:98b8fbf5-33f0-4470-88b0-39a9d526b115

Student theses

master thesis

© 2023 Ivar de Bruin