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="gamma" notice="2015-01"/>),
  25       <rlink to="download/lddl.tar.bz2">data set</rlink> (updated <notice class="gamma" notice="2014-12"/>),
  26       <rlink to="xml/">HELM server URL</rlink> (updated <notice class="gamma" notice="2014-12"/>).
  27    </topitem>
  28    <topitem name="examples">
  29       <notice class="alpha" notice="Examples:"/>
  30       <rlink to="static/lddl/Environment/grundlagen_2/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
  31          Grundlagen's definition "t234"</rlink>
  32       in λδ version 4.
  33    </topitem>
  34
  35    <subsection name="helena"><helena-icon/>Helena</subsection>
  36    <body>
  37       Helena is a processor for λδ,
  38       implemented in <link to="http://caml.inria.fr/">Caml</link>
  39       as a part of the <link to="http://helm.cs.unibo.it/">HELM</link> software,
  40       meant for testing the stable features of the calculus as well as the unstable ones.
  41    </body>
  42    <body>
  43       The processor source code is available in the directory
  44       <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>
  45       of the <link to="http://helm.cs.unibo.it/software/index.html">HELM Svn repository</link>.
  46       The Svn revisions containing the stable versions of Helena are indicated next.
  47    </body>
  48    <topitem name="v2">
  49       <notice class="gamma" notice="Version 0.8.2 (2014-12)."/>
  50       Uses λδ "Version 3" with layer variables as core language.
  51       Supports exportation to Grafite
  52       (the specification language of <link to="http://matita.cs.unibo.it/">Matita</link>).
  53       The overall validation speed of the "Grundlagen der Analysis"
  54       increases of 34% with respect to version 0.8.1.
  55       [Svn revision: 13005] (<rlink to="download/helena_0.8.2.tar.gz">archived source code</rlink>)
  56       <list><item>
  57          The specification of Landau's "Grundlagen der Analysis"
  58          for <link to="http://matita.cs.unibo.it/">Matita 0.99.2</link>:
  59          <rlink to="download/grundlagen_2.tar.bz2">grundlagen_2.tar.bz2</rlink>
  60          (revised <notice class="gamma" notice="2014-12"/>).
  61       </item><item>
  62          The corrected specification of Landau's "Grundlagen der Analysis":
  63          <rlink to="download/grundlagen_2.aut">grundlagen_2.aut</rlink>
  64          (revised <notice class="gamma" notice="2014-12"/>).
  65       </item><item>
  66          <notice class="gamma" notice="2014-12."/>
  67          The corrected specification of Landau's "Grundlagen der Analysis"
  68          is successfully validated in λδ "Version 3".
  69       </item></list>
  70    </topitem>
  71    <topitem name="v1">
  72       <notice class="beta" notice="Version 0.8.1 (2010-11)."/>
  73       Uses a subset of λδ "Version 4" as intermediate language.
  74       Features importation from ".hln" files containing λδ textual syntax.
  75       The overall validation speed of the "Grundlagen der Analysis"
  76       increases of 22% with respect to version 0.8.0.
  77       [Svn revision: 11032] (<rlink to="download/helena_0.8.1.tar.gz">archived source code</rlink>)
  78       <list><item>
  79          A <link to="http://www.jedsoft.org/jed/">Jed mode</link>
  80          for editing ".hln" files (containing λδ textual syntax):
  81          <rlink to="download/helena.sl">helena.sl</rlink>
  82          (revised <notice class="alpha" notice="2010-11"/>).
  83       </item><item>
  84          <notice class="beta" notice="2009-12."/>
  85          Helena appears in F. Wiedijk's
  86          <link to="http://www.cs.ru.nl/%7Efreek/digimath/index.html#helena">
  87             index of computer math systems</link>.
  88       </item></list>
  89    </topitem>
  90    <topitem name="v0">
  91       <notice class="beta" notice="Version 0.8.0 (2009-09)."/>
  92       Supports λδ "Version 2" with naive implementation of impredicative sort inclusion.
  93       Features importation from <link to="http://www.win.tue.nl/automath/">Automath</link>
  94       and exportation to <link to="http://www.w3.org/XML/">XML</link>.
  95       <rlink to="documentation.html#ldR4">Documentation (R4)</rlink>.
  96       [Svn revision: 10304] (<rlink to="download/helena_0.8.0.tar.gz">archived source code</rlink>).
  97       <list><item>
  98          A <link to="http://www.jedsoft.org/jed/">Jed mode</link>
  99          for editing ".aut" files
 100          (containing <link to="http://www.win.tue.nl/automath/">Automath</link> textual syntax):
 101          <rlink to="download/automath.sl">automath.sl</rlink>
 102          (revised <notice class="gamma" notice="2008-07"/>).
 103       </item><item>
 104          <notice class="beta" notice="2009-09."/>
 105          Jutting's specification of Landau's "Grundlagen der Analysis"
 106          enters λδ Digital Library.
 107       </item><item>
 108          <notice class="beta" notice="2009-06."/>
 109          Jutting's specification of Landau's "Grundlagen der Analysis"
 110          is successfully processed, enabling sort inclusion.
 111       </item></list>
 112    </topitem>
 113    <footer/>
 114 </page>