A practical module system for LF

Module systems for proof assistants provide administrative support for large developments when mechanizing the meta-theory of programming languages and logics. We describe a module system for the logical framework LF that is based on two main primitives: signatures and signature morphisms. Signatures are defined as collections of constant declarations, and signature morphisms as homo-morphism in between them. Our design is semantically transparent in the sense that it is always possible to elaborate modules into the module free version of LF. We have implemented our design as part of the Twelf system and rewritten parts of the Twelf example library to take advantage of the module system.