A 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.
In this paper we describe a module system for the logical framework LF. It is based on two main primitives: signatures and signature morphisms, which provide a semantically transparent module level and permit to represent logic translations as homomorphisms. Modular LF is a conservative extension over LF, and integrates an elaboration of modular into core LF signatures. We have implemented our design in the Twelf system and used it to modularize large parts of the Twelf example library.
svn co https://cvs.concert.cs.cmu.edu/twelf/branches/twelf-mod
make smlnj. For more information how to install and use Twelf, refer to the Twelf project homepage. Enjoy.