A New Internet-Draft is available from the on-line Internet-Drafts
directories.
Title : Logiweb Protocol Version 1
Author(s) : K. Grue
Filename : draft-grue-logiweb-protocol-1-00.txt
Pages : 27
Date : 2007-4-2
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.
A URL for this Internet-Draft is:
http://www.ietf.org/internet-drafts/draft-grue-logiweb-protocol-1-00.txt
To remove yourself from the I-D Announcement list, send a message to
i-d-announce-request@ietf.org with the word unsubscribe in the body of
the message.
You can also visit https://www1.ietf.org/mailman/listinfo/I-D-announce
to change your subscription settings.
Internet-Drafts are also available by anonymous FTP. Login with the
username "anonymous" and a password of your e-mail address. After
logging in, type "cd internet-drafts" and then
"get draft-grue-logiweb-protocol-1-00.txt".
A list of Internet-Drafts directories can be found in
http://www.ietf.org/shadow.html
or ftp://ftp.ietf.org/ietf/1shadow-sites.txt
Internet-Drafts can also be obtained by e-mail.
Send a message to:
mailserv@ietf.org.
In the body type:
"FILE /internet-drafts/draft-grue-logiweb-protocol-1-00.txt".
NOTE: The mail server at ietf.org can return the document in
MIME-encoded form by using the "mpack" utility. To use this
feature, insert the command "ENCODING mime" before the "FILE"
command. To decode the response(s), you will need "munpack" or
a MIME-compliant mail reader. Different MIME-compliant mail readers
exhibit different behavior, especially when dealing with
"multipart" MIME messages (i.e. documents which have been split
up into multiple messages), so check your local documentation on
how to manipulate these messages.
Below is the data which will enable a MIME compliant mail reader
implementation to automatically retrieve the ASCII version of the
Internet-Draft.
- <ftp://ftp.ietf.org/internet-drafts/draft-grue-logiweb-protocol-1-00.txt>
-
_______________________________________________
I-D-Announce@ietf.org
https://www1.ietf.org/mailman/listinfo/i-d-announce
