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 (2015-02)."/>
  50       Uses λδ "Version 3" with layer variables as core language.
  51       Supports exportation to Gallina
  52       (the specification language of <link to="http://coq.inria.fr/">Coq</link>),
  53       and to Grafite
  54       (the specification language of <link to="http://matita.cs.unibo.it/">Matita</link>).
  55       The overall validation speed of the "Grundlagen der Analysis"
  56       increases of 34% with respect to version 0.8.1.
  57       <rlink to="documentation.html#ldJ4">Documentation (J4)</rlink>.
  58       [Svn revision: 13035] (<rlink to="download/helena_0.8.2.tar.gz">archived source code</rlink>).
  59       <list><item>
  60          The specification of Landau's "Grundlagen der Analysis"
  61          for <link to="http://coq.inria.fr/">Coq 8</link>:
  62          <rlink to="download/grundlagen_2.v">grundlagen_2.v</rlink>
  63          (revised <notice class="gamma" notice="2015-02"/>).
  64       </item><item>
  65          The specification of Landau's "Grundlagen der Analysis"
  66          for <link to="http://matita.cs.unibo.it/">Matita 0.99.2</link>:
  67          <rlink to="download/grundlagen_2.tar.bz2">grundlagen_2.tar.bz2</rlink>
  68          (revised <notice class="gamma" notice="2015-02"/>).
  69       </item><item>
  70          The corrected specification of Landau's "Grundlagen der Analysis":
  71          <rlink to="download/grundlagen_2.aut">grundlagen_2.aut</rlink>
  72          (revised <notice class="gamma" notice="2014-12"/>).
  73       </item><item>
  74          <notice class="gamma" notice="2015-02."/>
  75          The translated specification of Landau's "Grundlagen der Analysis"
  76          is successfully validated in λC by <link to="http://coq.inria.fr/">Coq 8.4.3</link>.
  77       </item><item>
  78          <notice class="gamma" notice="2014-12."/>
  79          The corrected specification of Landau's "Grundlagen der Analysis"
  80          is successfully validated in λδ "Version 3".
  81       </item></list>
  82    </topitem>
  83    <topitem name="v1">
  84       <notice class="beta" notice="Version 0.8.1 (2010-11)."/>
  85       Uses a subset of λδ "Version 4" as intermediate language.
  86       Features importation from ".hln" files containing λδ textual syntax.
  87       The overall validation speed of the "Grundlagen der Analysis"
  88       increases of 22% with respect to version 0.8.0.
  89       [Svn revision: 11032] (<rlink to="download/helena_0.8.1.tar.gz">archived source code</rlink>).
  90       <list><item>
  91          A <link to="http://www.jedsoft.org/jed/">Jed mode</link>
  92          for editing ".hln" files (containing λδ textual syntax):
  93          <rlink to="download/helena.sl">helena.sl</rlink>
  94          (revised <notice class="alpha" notice="2010-11"/>).
  95       </item><item>
  96          <notice class="beta" notice="2009-12."/>
  97          Helena appears in F. Wiedijk's
  98          <link to="http://www.cs.ru.nl/%7Efreek/digimath/index.html#helena">
  99             index of computer math systems</link>.
 100       </item></list>
 101    </topitem>
 102    <topitem name="v0">
 103       <notice class="beta" notice="Version 0.8.0 (2009-09)."/>
 104       Supports λδ "Version 2" with naive implementation of impredicative sort inclusion.
 105       Features importation from <link to="http://www.win.tue.nl/automath/">Automath</link>
 106       and exportation to <link to="http://www.w3.org/XML/">XML</link>.
 107       <rlink to="documentation.html#ldR4">Documentation (R4)</rlink>.
 108       [Svn revision: 10304] (<rlink to="download/helena_0.8.0.tar.gz">archived source code</rlink>).
 109       <list><item>
 110          A <link to="http://www.jedsoft.org/jed/">Jed mode</link>
 111          for editing ".aut" files
 112          (containing <link to="http://www.win.tue.nl/automath/">Automath</link> textual syntax):
 113          <rlink to="download/automath.sl">automath.sl</rlink>
 114          (revised <notice class="gamma" notice="2008-07"/>).
 115       </item><item>
 116          <notice class="beta" notice="2009-09."/>
 117          Jutting's specification of Landau's "Grundlagen der Analysis"
 118          enters λδ Digital Library.
 119       </item><item>
 120          <notice class="beta" notice="2009-06."/>
 121          Jutting's specification of Landau's "Grundlagen der Analysis"
 122          is successfully processed, enabling sort inclusion.
 123       </item></list>
 124    </topitem>
 125    <footer/>
 126 </page>