Gloss of "FDL"

We imagine a Formal Digital Library as a repository for formally verified material along with other complementary material, much of which is essential for practical use of the formal. The complementary material is either unverified, only partially verified, or perhaps not subject to verification by machines. Further, we conceive of the FDL as a process for maintaining, accessing, and modifying the repository.

Actually we usually mean here an architecture suitable as a basis for building such libraries, and use the term (the "L" part anyway) with some reservations, but it continually indicates one of our main intentions.

One should expect that multiple independent FDLs of this sort will be created, some maintained long term, others quite temporarily, and that they should be able to communicate their content usefully.

Among the content of an FDL are specifications for how to verify formal content. It is not part of the FDL design to govern what counts as legitimate validation, and indeed FDLs are intended to be radically open. This requires accounting for what has been verified and by what means.

Different implementations of FDLs are possible and expected, and they may provide different services beyond the minimal, as well as have their own policies for access and contribution.

See Impartiality, Formal vs Informal, Logical Libraries IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html