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.
Last modified: Thu Jan 4 15:33:28 2007