A simple module system for LF

The logical framework LF (sometimes called the Edinburgh Logical
Framework) has formed the basis for the systems Elf and (more
recently) Twelf. These systems combine the declarative reading of LF
signatures as specifications for object logics, and an operational
reading of LF signatures as logic programs. Proof checking is
supported under the first interpretation, and proof search and logic
programming under the second.

Under both interpretations of LF signatures, one would like to be able
to present object logics in a modular and compositional way, and to be
able to reason about the interrelationships between various object
theories. Purely at the syntactic level, there is also a need for a
structured namespace in order to avoid name conflicts. The current
Twelf implementation does not yet support such a module system,
despite the fact that a module system for LF with an explicit calculus
of realizers has been proposed [Harper & Pfenning 98].

In this talk, I will try to motivate a simpler design, based on de
Bruijn's observation [de Bruijn 91] that a logical framework should
be as weak as possible. The system permits the definition of object
theories each in their own namespace, as well as reasoning about
extensions of such theories, and a notion of "functor" which realizes
one theory in terms of another. The system is intentionally designed
to be as weak as possible; all module-level constructs can be
rewritten in terms of pure LF constructs by a process of elaboration.
We plan to experiment with an extension of the Twelf implementation
supporting the new module system in the near future.

de Bruijn, N. [1991], A plea for weaker frameworks, in G. Huet and
G. Plotkin, eds, `Logical Frameworks', Cambridge University Press,
pp. 40-67.

Harper, R. and Pfenning, F. [1998] `A module system for a programming
language based on the LF logical framework', Journal of Logic and
Computation 8(1), 5-31.