<![CDATA[
<!-- For best results, you should include the HTML-coded -->
<!-- metadata that you find further down the page -->
<!-- (below the line) in the <HEAD></HEAD>-tag of your -->
<!-- page. This will simplify correct indexing by robots. -->
<!-- ---------------------------------------------------- -->
<META NAME="DC.Title" CONTENT="Certified and Portable Mathematical Documents from Formal Contexts ">
<LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#title">
<META NAME="DC.Creator.PersonalName" CONTENT="Caprotti, Olga">
<LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#creator">
<META NAME="DC.Creator.PersonalName.2" CONTENT="Geuvers, Herman">
<LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#creator">
<META NAME="DC.Creator.PersonalName.3" CONTENT="Oostdijk, Martijn">
<LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#creator">
<META NAME="DC.Subject" CONTENT="OpenMath">
<LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#subject">
<META NAME="DC.Subject" CONTENT="Formal Mathematics">
<LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#subject">
<META NAME="DC.Subject" CONTENT="Type Theory">
<LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#subject">
<META NAME="DC.Subject" SCHEME="CCS" CONTENT="H.5.4">
<LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#subject">
<META NAME="DC.Subject" SCHEME="CCS" CONTENT="I.7.2">
<LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#subject">
<META NAME="DC.Subject" SCHEME="CCS" CONTENT="I.2.3">
<LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#subject">
<META NAME="DC.Description" CONTENT=" 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.">
<LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#description">
<META NAME="DC.Publisher" CONTENT="RISC-Linz, Johannes Kepler University, Austria">
<LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#publisher">
<META NAME="DC.Date" SCHEME="ISO8601" CONTENT="2001-09-24">
<LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#date">
<META NAME="DC.Type" CONTENT="Text.Article">
<LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#type">
<META NAME="DC.Format" SCHEME="IMT" CONTENT="application/postscript">
<LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#format">
<LINK REL=SCHEMA.imt HREF="http://sunsite.auc.dk/RFC/rfc/rfc2046.html">
<META NAME="DC.Format.X-Carrier" CONTENT="file">
<LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#format">
<META NAME="DC.Identifier" SCHEME="URL" CONTENT="http://www.risc.uni-linz.ac.at/people/ocaprott/Proceedings/printed/caprotti.ps">
<LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#identifier">
<META NAME="DC.Language" SCHEME="ISO639-1" CONTENT="en">
<LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#language">
<META NAME="EULER.Event.Location" CONTENT="RISC-Linz, A-4232 Schloss Hagenberg">
<LINK REL=SCHEMA.dc HREF="http://www.lub.lu.se/EULER/partners/april99-metadatacreator.html">
<META NAME="EULER.Event.Date" SCHEME="ISO8601" CONTENT="2001-09-24">
<LINK REL=SCHEMA.dc HREF="http://www.lub.lu.se/EULER/partners/april99-metadatacreator.html">
<META NAME="EULER.Event.Name" CONTENT="First International Workshop on Mathematical Knowledge Management">
<LINK REL=SCHEMA.dc HREF="http://www.lub.lu.se/EULER/partners/april99-metadatacreator.html">
<META NAME="DC.Date.X-MetadataLastModified" SCHEME="ISO8601" CONTENT="2001-10-25">
<LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#date">
]]>