IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
Borrowed Certificates
In Certificate Structure it is explained how creation and update code are determined for "native" certificate identifiers. Here we explain how certificates are borrowed from other purported FDLs.
A certificate with kind <C,K>, where C is classified by the FDL as indicating a borrowed rather than a native certificate, cannot be updated -- reconsideration of borrowed certificates always fails, which means that if they get in the way they should be replaced by native certificates. When one wishes to locally "re-establish" a borrowed certificate, one requests the creation of a native certificate stipulating a native certificate id C' which one thinks will execute the native code of K similarly to the way the foreign FDL is supposed to have interpreted it. FDLs that hope to cooperate and share Clients would do well to provide a standard collection of similar native languages and interpreters; multiple instances of a common implementation will, of course, minimize coding in this regard.
A certificate with kind <C,K>, where C is a borrowed-certificate identifier, is created by Merging a Closed Map from a foreign FDL into the local FDL. When a merge is attempted one specifies a correspondence between objects that should be identified. If one stipulates that certificate id C in the local FDL is to be identified with C' of the foreign FDL, then the merge fails if any
new certificates of kind C would have gotten imported; ie, foreign certificate ids can only be identified with native certificates ids if the certificates depending on them were already in the local FDL.
How can a cross-FDL correspondence between identifiers, certificate identifiers in this case, be established when each space of identifiers is "internal" to its own FDL? In general, a Client of an FDL might establish an association between abstract identifiers of the FDL and other values (which might themselves be either concrete values or abstract identifiers), by storing in the FDL a text serving as a table pairing the values with the abstract identifiers. One FDL, say A, could borrow from another FDL, say B, by becoming its Client and creating two tables, one in A and another in B. One concrete value for each cross-FDL abstract id pair would be generated, and these values would mediate the two tables in A and B.
Establishing such cross-FDL abstract identifier correspondences, to facilitate certificate borrowing or other content sharing more generally, should be so common that it should be "internalized" as an FDL service and obviate the need for exposing the intermediate concrete values that coordinate cross-FDL pairings. Further, significant efficiencies are likely in explicitly recognizing a mutual client relationship between FDLs. Hence there is a special role for FDLs as clients of other FDLs, essentially supporting federation, that is worth making efficient.
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html