Skip to main content
PRL Project

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.