Designing a Logical Library
by Stuart F. Allen
1996-1997
Maintaining a library of objects including proofs, definitions, and tactic code, with logically significant interdependencies them will become key to systems such a Nuprl. Some semantically and practically motivated design issues will be discussed.