TITLE of the resource to be described

 

Alternative title (Titles other than main title)

 

CREATOR (Name of the person or organization primarily responsible for creating the intellectual content)

Creator name Personal name: "Last, First" Corporate name

Creator name Personal name: "Last, First" Corporate name

Creator name Personal name: "Last, First" Corporate name

 

SUBJECT: Keywords (Your own keywords describing the topic of the resource, one per box)

 

SUBJECT: Classification (Notations for the resource, one per box)

Dewey Decimal Classification ACM Computing Classification System

Dewey Decimal Classification ACM Computing Classification System

Dewey Decimal Classification ACM Computing Classification System

 

DESCRIPTION (Abstract, content description)

This paper deals with the problem of generating interactive natural language documents based on formal mathematics. It describes how formal mathematical developments, carried out in the type theoretical theorem prover coq, can be transformed to readable and interactive documents viewable using standard Web browser technology. The transformation process produces documents encoded in an xml application called OmDoc, suited for describing mathematical documents.

 

PUBLISHER (University department, corporate entity etc.)

 

DATE (Date associated with the creation or availability of the resource)

  1996-09-23 (ISO 8601) 19960923 (ANSI.X3.30-1985) Mon, 23 Sep 1996 (RFC 822)

 

TYPE (Category of the resource)

Text Text.Abstract Text.Advertisement Text.Article Text.Correspondence Text.Correspondence.Discussion Text.Correspondence.Email Text.Correspondence.Letter Text.Correspondence.Postcard Text.Dictionary Text.Form Text.Homepage Text.Homepage.Organizational Text.Homepage.Personal Text.Index Text.Manuscript Text.Minutes Text.Monograph Text.Pamphlet Text.Poem Text.Proceedings Text.Promotion Text.Serial Text.Serial.Journal Text.Serial.Magazine Text.Serial.Newsletter Text.Serial.Newspaper Text.TechReport Text.Thesis Text.Thesis.Doctoral Text.Thesis.Masters Image Image.Moving Image.Moving.Animation Image.Moving.Film Image.Photograph Image.Graphic Sound Sound.Ambient Sound.Effect Sound.Music Sound.Narration Sound.Speech Software Software.Executable Software.Source Data Data.Numeric Data.Spatial Data.Spectral Data.Statistical Data.Structured-Text Interactive Interactive.Chat Interactive.Games Interactive.Multimedia Interactive.VR

 

FORMAT (Data representation of the resource, MIME type)

text/html (.htm, .html) application/msword (.doc) application/pdf (.pdf) application/postscript (.ai, .eps, .ps) application/powerpoint (.ppt) application/rtf (.rtf) application/wordperfect5.1 application/x-latex (.latex) image/gif (.gif) image/jpeg (.jpeg, .jpe, .jpg) text/plain (.txt) text/x-sgml (.sgml, .sgm)

 

Physical carrier (Physical carrier of information)

Printed material (paper) Hand-written material Letters Internet file Film Computerreadable material Microfilm Microfiche Media combination Multimedia CD-ROM

 

URN (URN of resource described in the record)

ISSN (Location of the document. Start with 'http://')

 

ISBN (Location of the document. Start with 'http://')

 

URL (Location of the document. Start with 'http://')

LANGUAGE of the content of the resource described

English Danish Finnish Icelandic Norwegian No: Nynorsk No: Bokmaal Swedish Northern Sámi Abkhazian Afar Afrikaans Albanian Amharic Arabic Armenian Assamese Aymara Azerbaijani Bashkir Basque Bengali; Bangla Bhutani Bihari Bislama Breton Bulgarian Burmese Byelorussian Cambodian Catalan Chinese Cornish Corsican Croatian Czech Dutch Esperanto Estonian Faroese Fiji French Frisian Galician Georgian German Greek Greenlandic Guarani Gujarati Hausa Hebrew Hindi Hungarian Indonesian Interlingua Interlingue Inuktitut Inupiak Irish (Irish Gaelic) Italian Japanese Javanese Kannada Kashmiri Kazakh Kinyarwanda Kirghiz Kirundi Korean Kurdish Laothian (Laotian) Latin Latvian; Lettish Lingala Lithuanian Luxemburgish Macedonian Malagasy Malay Malayalam Maltese Manx Gaelic Maori Marathi Moldavian Mongolian Nauru Nepali Occitan Oriya Oromo (Afan) Pashto; Pushto Persian Polish Portuguese Punjabi Quechua Rhaeto-Romance Romanian Russian Samoan Sangho Sanskrit Scots Gaelic (Scottish Gaelic) Serbian Serbo-Croatian Sesotho Setswana Shona Sindhi Singhalese Siswati Slovak Slovenian Somali Spanish Sudanese Swedish Swahili Tagalog Tajik Tamil Tatar Telugu Thai Tibetan Tigrinya Tonga Tsonga Turkish Turkmen Twi Uigur Ukrainian Urdu Uzbek Vietnamese Volapük Welsh Wolof Xhosa Yiddish Yoruba Zhuang Zulu

 

Terms and Conditions (Link to a copyright notice etc.)

 

EULER identifier (Extra identification of the resource)

 

Event location (Location of event for/at which the resource described was created)

 

Event date (Date [YYYY-MM-DD] of event for/at which the resource described was created)

 

Event name (Name of event where resource described was created)

 

for preview for inclusion in HTML-document for inclusion in HTML4-document

Additional DC-elements

CONTRIBUTOR (Name of significant contributors other than the creator)
SUBJECT: Controlled vocabulary (Keywords from established schemes, one per box)
SUBJECT: MSC Classification (Notations for the resource, one per box)