The model of distribution

• The validity of a mathematical document A that refers to a document B can be guaranteed only if B does not change ===> mathematical documents should be immutable

• Conjectures could be prooved, theories could be augmented ===> new versions of a document could be released

• We cannot force users to maintain forever the documents they have written (and in the same place) ===> need for logical names (URIs) instead of phisical names (URLs) (e.g. "cic:/coq/INIT/Datatypes/nat.ind")