]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/www/lambdadelta/web/home/implementation.ldw.xml
projects / helm.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
\lambda\delta web site update for git
[helm.git] / helm / www / lambdadelta / web / home / implementation.ldw.xml
diff --git a/helm/www/lambdadelta/web/home/implementation.ldw.xml b/helm/www/lambdadelta/web/home/implementation.ldw.xml
index b8cc30553b3f5b04af6fd5ddeef9451ca87d37c3..76bd89b33a94626779f64dd34c101189cb5099bd 100644 (file)
--- a/helm/www/lambdadelta/web/home/implementation.ldw.xml
+++ b/helm/www/lambdadelta/web/home/implementation.ldw.xml
@@ -3,48 +3,31 @@
 <page xmlns="http://lambdadelta.info/"
       description = "\lambda\delta home page"
       title = "\lambda\delta home page"
 <page xmlns="http://lambdadelta.info/"
       description = "\lambda\delta home page"
       title = "\lambda\delta home page"
-      head = "The Formal System λδ (\lambda\delta)"
+      logo = "crux"
+      head = "The Formal Systems of the λδ (\lambda\delta) Family"
 >
    <sitemap name="sitemap"/>
 
 >
    <sitemap name="sitemap"/>
 
-   <section9 name="specifications">Computer-checked formal specifications</section9>
-   <body>
-      λδ comes in several versions listed in the following table,
-      which includes the major milestones:
-   </body>
-   <table name="versions"/>
-
    <section5 name="tools">Tools</section5>
 
    <section5 name="tools">Tools</section5>
 
-   <section name="lddl"><crux-icon/>λδ Digital Library (LDDL)</section>
+   <subsection name="osn"><img logo="osn"/>Open Symbolic Notation</subsection>
+
    <body>
    <body>
-      The λδ Digital Library is part of <link to="http://helm.cs.unibo.it/">HELM</link>
-      and contains resources expressed in λδ.      
+      Open Symbolic Notation, abbreviated OSN,
+      is an easy and flexible data-interchange text format
+      intended for the lightweight representation of
+      generic abstract syntax trees in the domain of formal languages.
+      Additional information is available at <rlink to="osn/">OSN web site</rlink>.
    </body>
    </body>
-   <news date="Contents:">
-      Landau's "Grundlagen der Analysis"
-      (from Jutting's specification in  <link to="http://www.win.tue.nl/automath/">Automath</link>).
-   </news>
-   <news date="Access:">
-      <rlink to="static/lddl/">static pages</rlink> (updated <date date="2012-10"/>),
-      <rlink to="download/lddl.tar.bz2">data set</rlink> (updated <date date="2012-10"/>),
-      <rlink to="xml/">HELM server URL</rlink> (updated <date date="2012-10"/>).
-   </news>
-   <news date="Examples:">
-      <rlink to="static/lddl/brg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
-         Grundlagen's definition "t234"</rlink>
-      (in "basic_rg" λδ),
-      <rlink to="static/lddl/crg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
-         Grundlagen's definition "t234"</rlink>
-      (in "complete_rg" λδ).
-   </news>
 
 
-   <section name="helena"><helena-icon/>Helena</section>
+
+   <subsection name="helena"><img logo="helena"/>Helena</subsection>
+
    <body>
    <body>
-      Helena is a λδ processor,
+      Helena is a processor for the systems of the λδ family,
       implemented in <link to="http://caml.inria.fr/">Caml</link>
       as a part of the <link to="http://helm.cs.unibo.it/">HELM</link> software,
       implemented in <link to="http://caml.inria.fr/">Caml</link>
       as a part of the <link to="http://helm.cs.unibo.it/">HELM</link> software,
-      meant for testing the stable features of the calculus as well as the unstable ones.
+      meant for testing both their stable and unstable features.
    </body>
    <body>
       The processor source code is available in the directory
    </body>
    <body>
       The processor source code is available in the directory
@@ -52,48 +35,129 @@
       of the <link to="http://helm.cs.unibo.it/software/index.html">HELM Svn repository</link>.
       The Svn revisions containing the stable versions of Helena are indicated next.
    </body>
       of the <link to="http://helm.cs.unibo.it/software/index.html">HELM Svn repository</link>.
       The Svn revisions containing the stable versions of Helena are indicated next.
    </body>
-   <news date="Version 0.8.2.">
-      In progress.
-   </news>
-   <news date="Version 0.8.1 (2010-11).">
-      Exploits a subset of "complete_rg" λδ as the intermediate language.
+
+   <topitem name="v3">
+      <notice class="gamma" notice="Version 0.8.3 (2015-12)."/>
+      Supports exportation to λProlog
+      (two formats for ELPI,
+      and two formats for <link to="http://teyjus.cs.umn.edu/">Teyjus</link>).
+      Employs optimized conditional compilation through
+      <link to="http://camlp5.gforge.inria.fr/">camlp5</link> code preprocessor (pa_macro)
+      to reduce a performance loss, which is expected to disappear
+      by employing a different code preprocessor.
+      Overall validation speed of the "Grundlagen der Analysis" with respect to version 0.8.2:
+      +3% with optimized compilation, +5% without optimized compilation.
+      [Svn revision: 13108] (<rlink to="download/helena_0.8.3.tar.gz">archived source code</rlink>).
+      <list><item>
+         <notice class="gamma" notice="2015-06."/>
+         The corrected specification of Landau's "Grundlagen der Analysis"
+         is successfully validated in a λProlog implementation of λδ version 3.
+      </item></list>
+   </topitem>
+
+   <topitem name="v2">
+      <notice class="gamma" notice="Version 0.8.2 (2015-02)."/>
+      Uses λδ version 3 with layer variables as core language.
+      Supports exportation to Gallina
+      (the specification language of <link to="http://coq.inria.fr/">Coq</link>),
+      and to Grafite
+      (the specification language of <link to="http://matita.cs.unibo.it/">Matita</link>).
+      The overall validation speed of the "Grundlagen der Analysis"
+      increases of 34% with respect to version 0.8.1.
+      <rlink to="html/documentation.html#ldJ3a">Documentation (J3a)</rlink>.
+      [Svn revision: 13035] (<rlink to="download/helena_0.8.2.tar.gz">archived source code</rlink>).
+      <list><item>
+         The specification of Landau's "Grundlagen der Analysis"
+         for <link to="http://coq.inria.fr/">Coq 8</link>:
+         <rlink to="download/grundlagen_2.v">grundlagen_2.v</rlink>
+         (revised <notice class="gamma" notice="2015-02"/>).
+      </item><item>
+         The specification of Landau's "Grundlagen der Analysis"
+         for <link to="http://matita.cs.unibo.it/">Matita 0.99.2</link>:
+         <rlink to="download/grundlagen_2.tar.bz2">grundlagen_2.tar.bz2</rlink>
+         (revised <notice class="gamma" notice="2015-02"/>).
+      </item><item>
+         The corrected specification of Landau's "Grundlagen der Analysis":  
+         <rlink to="download/grundlagen_2.aut">grundlagen_2.aut</rlink>
+         (revised <notice class="gamma" notice="2014-12"/>).
+      </item><item>
+         <notice class="gamma" notice="2015-02."/>
+         The translated specification of Landau's "Grundlagen der Analysis"
+         is successfully validated in CC by <link to="http://coq.inria.fr/">Coq 8.4.3</link>.
+      </item><item>
+         <notice class="gamma" notice="2014-12."/>
+         The corrected specification of Landau's "Grundlagen der Analysis"
+         is successfully validated in λδ version 3.
+      </item></list>
+   </topitem>
+
+   <topitem name="v1">
+      <notice class="beta" notice="Version 0.8.1 (2010-11)."/>
+      Uses a subset of λδ version 4 as intermediate language.
       Features importation from ".hln" files containing λδ textual syntax.
       The overall validation speed of the "Grundlagen der Analysis"
       Features importation from ".hln" files containing λδ textual syntax.
       The overall validation speed of the "Grundlagen der Analysis"
-      increases of 22% with respect toversion 0.8.0.
-      [Svn revision: 11032] (<rlink to="download/helena_0.8.1.tar.gz">archived source code</rlink>)
+      increases of 22% with respect to version 0.8.0.
+      [Svn revision: 11032] (<rlink to="download/helena_0.8.1.tar.gz">archived source code</rlink>).
       <list><item>
          A <link to="http://www.jedsoft.org/jed/">Jed mode</link>
          for editing ".hln" files (containing λδ textual syntax):
          <rlink to="download/helena.sl">helena.sl</rlink>
       <list><item>
          A <link to="http://www.jedsoft.org/jed/">Jed mode</link>
          for editing ".hln" files (containing λδ textual syntax):
          <rlink to="download/helena.sl">helena.sl</rlink>
-         (revised <date date="2010-11"/>).
+         (revised <notice class="alpha" notice="2010-11"/>).
       </item><item>
       </item><item>
-         <date date="2009-12."/>
+         <notice class="beta" notice="2009-12."/>
          Helena appears in F. Wiedijk's
          <link to="http://www.cs.ru.nl/%7Efreek/digimath/index.html#helena">
             index of computer math systems</link>.
       </item></list>
          Helena appears in F. Wiedijk's
          <link to="http://www.cs.ru.nl/%7Efreek/digimath/index.html#helena">
             index of computer math systems</link>.
       </item></list>
-   </news>
-   <news date="Version 0.8.0 (2009-09).">
-      Supports "basic_rg" λδ with naive implementation of impredicative sort inclusion.
+   </topitem>
+
+   <topitem name="v0">
+      <notice class="beta" notice="Version 0.8.0 (2009-09)."/>
+      Supports λδ version 2 with naive implementation of impredicative sort inclusion.
       Features importation from <link to="http://www.win.tue.nl/automath/">Automath</link>
       and exportation to <link to="http://www.w3.org/XML/">XML</link>.
       Features importation from <link to="http://www.win.tue.nl/automath/">Automath</link>
       and exportation to <link to="http://www.w3.org/XML/">XML</link>.
-      <rlink to="documentation.html#ldp6">Documentation</rlink>.
+      <rlink to="html/documentation.html#ldR2a">Documentation (R2a)</rlink>.
       [Svn revision: 10304] (<rlink to="download/helena_0.8.0.tar.gz">archived source code</rlink>).
       <list><item>
          A <link to="http://www.jedsoft.org/jed/">Jed mode</link>
          for editing ".aut" files
          (containing <link to="http://www.win.tue.nl/automath/">Automath</link> textual syntax):
          <rlink to="download/automath.sl">automath.sl</rlink>
       [Svn revision: 10304] (<rlink to="download/helena_0.8.0.tar.gz">archived source code</rlink>).
       <list><item>
          A <link to="http://www.jedsoft.org/jed/">Jed mode</link>
          for editing ".aut" files
          (containing <link to="http://www.win.tue.nl/automath/">Automath</link> textual syntax):
          <rlink to="download/automath.sl">automath.sl</rlink>
-         (revised <date date="2008-07"/>).
+         (revised <notice class="gamma" notice="2008-07"/>).
       </item><item>
       </item><item>
-         <date date="2009-09."/>
+         <notice class="beta" notice="2009-09."/>
          Jutting's specification of Landau's "Grundlagen der Analysis"
          enters λδ Digital Library.
       </item><item>
          Jutting's specification of Landau's "Grundlagen der Analysis"
          enters λδ Digital Library.
       </item><item>
-         <date date="2009-06."/>
+         <notice class="beta" notice="2009-06."/>
          Jutting's specification of Landau's "Grundlagen der Analysis"
          is successfully processed, enabling sort inclusion.
       </item></list>
          Jutting's specification of Landau's "Grundlagen der Analysis"
          is successfully processed, enabling sort inclusion.
       </item></list>
-   </news>
+   </topitem>
+
+   <subsection name="lddl"><img logo="lddl"/>λδ Digital Library (LDDL)</subsection>
+
+   <body>
+      The λδ Digital Library is part of <link to="http://helm.cs.unibo.it/">HELM</link>
+      and contains resources expressed in the systems of the λδ family.      
+   </body>
+   <topitem name="contents">
+      <notice class="alpha" notice="Contents:"/>
+      Landau's "Grundlagen der Analysis"
+      (from Jutting's specification in  <link to="http://www.win.tue.nl/automath/">Automath</link>).
+   </topitem>
+   <topitem name="access">
+      <notice class="alpha" notice="Access:"/>
+      <rlink to="static/lddl/">static pages</rlink> (updated <notice class="gamma" notice="2015-01"/>),
+      <rlink to="download/lddl.tar.bz2">data set</rlink> (updated <notice class="gamma" notice="2014-12"/>),
+      <rlink to="xml/">HELM server URL</rlink> (updated <notice class="gamma" notice="2014-12"/>).
+   </topitem>
+   <topitem name="examples">
+      <notice class="alpha" notice="Examples:"/>
+      <rlink to="static/lddl/Environment/grundlagen_2/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
+         Grundlagen's definition "t234"</rlink>
+      in λδ version 4.
+   </topitem>
+
    <footer/>
 </page>
    <footer/>
 </page>
Unnamed repository; edit this file 'description' to name the repository.