helm/www/lambdadelta/web/home/implementation.ldw.xml

   1 <?xml version="1.0" encoding="UTF-8"?>
   2
   3 <page xmlns="http://lambdadelta.info/"
   4       description = "\lambda\delta home page"
   5       title = "\lambda\delta home page"
   6       head = "The Formal System λδ (\lambda\delta)"
   7 >
   8    <sitemap name="sitemap"/>
   9
  10    <section5 name="tools">Tools</section5>
  11
  12    <subsection name="lddl"><crux-icon/>λδ Digital Library (LDDL)</subsection>
  13    <body>
  14       The λδ Digital Library is part of <link to="http://helm.cs.unibo.it/">HELM</link>
  15       and contains resources expressed in λδ.
  16    </body>
  17    <topitem name="contents">
  18       <notice class="alpha" notice="Contents:"/>
  19       Landau's "Grundlagen der Analysis"
  20       (from Jutting's specification in  <link to="http://www.win.tue.nl/automath/">Automath</link>).
  21    </topitem>
  22    <topitem name="access">
  23       <notice class="alpha" notice="Access:"/>
  24       <rlink to="static/lddl/">static pages</rlink> (updated <notice class="beta" notice="2012-10"/>),
  25       <rlink to="download/lddl.tar.bz2">data set</rlink> (updated <notice class="beta" notice="2012-10"/>),
  26       <rlink to="xml/">HELM server URL</rlink> (updated <notice class="beta" notice="2012-10"/>).
  27    </topitem>
  28    <topitem name="examples">
  29       <notice class="alpha" notice="Examples:"/>
  30       <rlink to="static/lddl/brg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
  31          Grundlagen's definition "t234"</rlink>
  32       (in "basic_rg" λδ),
  33       <rlink to="static/lddl/crg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
  34          Grundlagen's definition "t234"</rlink>
  35       (in "complete_rg" λδ).
  36    </topitem>
  37
  38    <subsection name="helena"><helena-icon/>Helena</subsection>
  39    <body>
  40       Helena is a λδ processor,
  41       implemented in <link to="http://caml.inria.fr/">Caml</link>
  42       as a part of the <link to="http://helm.cs.unibo.it/">HELM</link> software,
  43       meant for testing the stable features of the calculus as well as the unstable ones.
  44    </body>
  45    <body>
  46       The processor source code is available in the directory
  47       <link to="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&amp;path=%2Ftrunk%2Fhelm%2Fsoftware%2Fhelena%2F&amp;rev=0&amp;sc=0">/trunk/helm/software/helena/</link>
  48       of the <link to="http://helm.cs.unibo.it/software/index.html">HELM Svn repository</link>.
  49       The Svn revisions containing the stable versions of Helena are indicated next.
  50    </body>
  51    <topitem name="v2">
  52       <notice class="beta" notice="Version 0.8.2."/>
  53       In progress.
  54    </topitem>
  55    <topitem name="v1">
  56       <notice class="beta" notice="Version 0.8.1 (2010-11)."/>
  57       Exploits a subset of "complete_rg" λδ as the intermediate language.
  58       Features importation from ".hln" files containing λδ textual syntax.
  59       The overall validation speed of the "Grundlagen der Analysis"
  60       increases of 22% with respect to version 0.8.0.
  61       [Svn revision: 11032] (<rlink to="download/helena_0.8.1.tar.gz">archived source code</rlink>)
  62       <list><item>
  63          A <link to="http://www.jedsoft.org/jed/">Jed mode</link>
  64          for editing ".hln" files (containing λδ textual syntax):
  65          <rlink to="download/helena.sl">helena.sl</rlink>
  66          (revised <notice class="alpha" notice="2010-11"/>).
  67       </item><item>
  68          <notice class="beta" notice="2009-12."/>
  69          Helena appears in F. Wiedijk's
  70          <link to="http://www.cs.ru.nl/%7Efreek/digimath/index.html#helena">
  71             index of computer math systems</link>.
  72       </item></list>
  73    </topitem>
  74    <topitem name="v0">
  75       <notice class="beta" notice="Version 0.8.0 (2009-09)."/>
  76       Supports "basic_rg" λδ with naive implementation of impredicative sort inclusion.
  77       Features importation from <link to="http://www.win.tue.nl/automath/">Automath</link>
  78       and exportation to <link to="http://www.w3.org/XML/">XML</link>.
  79       <rlink to="documentation.html#ldR4">Documentation (R4)</rlink>.
  80       [Svn revision: 10304] (<rlink to="download/helena_0.8.0.tar.gz">archived source code</rlink>).
  81       <list><item>
  82          A <link to="http://www.jedsoft.org/jed/">Jed mode</link>
  83          for editing ".aut" files
  84          (containing <link to="http://www.win.tue.nl/automath/">Automath</link> textual syntax):
  85          <rlink to="download/automath.sl">automath.sl</rlink>
  86          (revised <notice class="gamma" notice="2008-07"/>).
  87       </item><item>
  88          <notice class="beta" notice="2009-09."/>
  89          Jutting's specification of Landau's "Grundlagen der Analysis"
  90          enters λδ Digital Library.
  91       </item><item>
  92          <notice class="beta" notice="2009-06."/>
  93          Jutting's specification of Landau's "Grundlagen der Analysis"
  94          is successfully processed, enabling sort inclusion.
  95       </item></list>
  96    </topitem>
  97    <footer/>
  98 </page>