A Module System for Agda

When designing the module system for the new version of Agda an important goal has been to make a clear distinction between modules and records. Records are typed first-class entities, whereas modules are simply collections of definitions. An advantage of this approach is that scope checking can be separated from type checking--no type checking is needed to figure out which names a module contains. Although simple, our module system supports a number of useful features: modules inside modules, parameterised modules (similar to sections in Coq), and separate type checking.

Presented at CHIT-CHAT 2007 in Nijmegen.
[slides]


Valid HTML 4.01! Disclaimer
Last modified: Thu Jan 4 15:33:28 2007