A Module System for LF A Module System for LF

Abstract

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.

Paper

A draft paper is available.

Twelf Sources

Mini-ML meta theory: mini-ml-variant.elf.
Kolmogorov translation: kolm.elf.
First-order Logic: fol.elf.
Algebra: algebra.elf.
Martin-Loef type theory mltt.elf.
Proof theory, model theory, and soundness of classical propositional logic pl-sound.elf.

Installation Instructions

To load the files, you will need a version of Twelf with a prototypical implementention of the module system. It can be accessed via

svn co https://cvs.concert.cs.cmu.edu/twelf/branches/twelf-mod

and compiled using make smlnj. For more information how to install and use Twelf, refer to the Twelf project homepage. Enjoy.
Last modified: Wed Jan 28 17:59:11 CET 2009