Logiweb Protocol Version 1
draft-grue-logiweb-protocol-1-01
| Document | Type |
Expired Internet-Draft
(individual)
Expired & archived
|
|
|---|---|---|---|
| Author | Klaus Grue | ||
| Last updated | 2007-08-06 | ||
| RFC stream | (None) | ||
| Intended RFC status | (None) | ||
| Formats | |||
| Stream | Stream state | (No stream defined) | |
| Consensus boilerplate | Unknown | ||
| RFC Editor Note | (None) | ||
| IESG | IESG state | Expired | |
| Telechat date | (None) | ||
| Responsible AD | (None) | ||
| Send notices to | (None) |
This Internet-Draft is no longer active. A copy of the expired Internet-Draft is available in these formats:
Abstract
When publishing mechanically verified mathematics on the Internet, there is a need for referencing previously published documents. As an example, referenced documents may contain needed definitions, lemmas, and proofs. References from one mechanically verified document to another is much like any other Uniform Resource Locator, but there is a need to ensure that referenced documents do not change after publication. This is so because otherwise a change of e.g. a definition in a referenced document could invalidate the correctness of a referencing document. The present document describes the protocol used by an experimental system named "Logiweb" which allows to publish mechanically verified, immutable mathematical documents.
Authors
(Note: The e-mail addresses provided for the authors of this Internet-Draft may no longer be valid.)