The basic model of working with Closed Maps is to maintain a "current closed map" as a part of state that is updated repeatedly as one works.

The FDL is a repository not of closed maps per se, but is rather a repository of data and instructions for building closed maps modulo choice of abstract identifiers.
One engages the FDL in a Session to help build and manipulate closed maps and also to store them for later retrieval (modulo closed map equivalence).

While there are useful notions of dependency between objects that may arise during a session as part of state outside the current closed map, the dependencies of enduring value shall be formulated purely in terms of closed maps (and treat indices abstractly).

Relatedly, while there are useful notions of correctness that can be defined with respect to state, the enduring ones shall be formulated in terms of closed maps alone. Further, while one can make good use of criteria of correctness of a proper submap of a closed map that depends upon the full closed map (say involving a search of the full closed map), we shall attach greater enduring value to those criteria for correctness of a closed map that depend only on that submap alone. Such criteria are preserved by monotonic extension of the closed map to a supermap.

Sometimes our criteria for correctness will depend on how programs (for example, Tactics) execute. Observe that when identifiers are treated abstractly by the computation system, they cannot be "secretly" computed. They must be provided as data to the computation either directly or via the current closed map. Further, since object indices are simple rather than complex, computation of object indices cannot be hidden by runtime combination.

Had we defined closed maps concretely as functions of type Text() or StringText(String) then program execution could create references to objects without its being apparent from the program code. Similarly, had we defined the closed maps as (A List)Text(A), even leaving the basic identifiers abstract but indexing objects by complexes, again one could "hide" the references to objects in the execution. IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html