]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/www/lambdadelta/web/home/specification.ldw.xml
projects / helm.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
λδ site update
[helm.git] / helm / www / lambdadelta / web / home / specification.ldw.xml
diff --git a/helm/www/lambdadelta/web/home/specification.ldw.xml b/helm/www/lambdadelta/web/home/specification.ldw.xml
index b88abf3a1c36290debcf6592226ffdc5ec4156b5..1b9486905620802207277b07081288efab5a68b6 100644 (file)
--- a/helm/www/lambdadelta/web/home/specification.ldw.xml
+++ b/helm/www/lambdadelta/web/home/specification.ldw.xml
@@ -3,109 +3,184 @@
 <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"/>
 
    <section15 name="specifications">Computer-checked formal specifications</section15>
    <body>
 >
    <sitemap name="sitemap"/>
 
    <section15 name="specifications">Computer-checked formal specifications</section15>
    <body>
-      λδ is developed as a machine-checked digital specification.
-      It comes in several versions listed in the next table,
-      which includes the major milestones.
+      The systems of the λδ family are developed as machine-checked digital specifications,
+      and are listed in the next table, which includes the major milestones.
    </body>
    <body>
       The life cycle of a specification consists of four periods.
    </body>
    <body>
       The life cycle of a specification consists of four periods.
-      <notice class="alpha" notice="Alpha:"/>
+      <notice class="alpha" text="Alpha:"/>
       the definitions are designed and the major propositions are proved,
       then the calculus is announced with a presentation.
       the definitions are designed and the major propositions are proved,
       then the calculus is announced with a presentation.
-      <notice class="beta" notice="Beta:"/>
+      <notice class="beta" text="Beta:"/>
       major changes and additions may occur before the calculus is released on paper.
       major changes and additions may occur before the calculus is released on paper.
-      <notice class="gamma" notice="Gamma:"/>
+      <notice class="gamma" text="Gamma:"/>
       subsequent improvements occur until the specification is completed or superseded,
       while major changes and additions are announced and reported on paper.
       subsequent improvements occur until the specification is completed or superseded,
       while major changes and additions are announced and reported on paper.
-      <notice class="delta" notice="Delta:"/>
-      after its conclusion, the specification is modified just for maintenance. 
+      <notice class="delta" text="Delta:"/>
+      after its conclusion, the specification is modified just for maintenance.
    </body>
    <table name="versions"/>
 
    </body>
    <table name="versions"/>
 
+   <body>
+     <notice class="alpha" text="Change logs: "/>
+     <rlink to="html/changes.html">System and Specification</rlink>
+     (updated <notice class="gamma" notice="2019-12"/>).
+   </body>
+
    <body>
      Informational pages on the specifications are provided.
    </body>
    <body>
      Informational pages on the specifications are provided.
    </body>
-   <topitem>
-      <notice class="alpha" notice="Notice on displayed numerical acounts:"/>
+   <topitem name="notice1">
+      <notice class="alpha" text="Notice on displayed numerical acounts:"/>
       nodes are counted according to the "intrinsic complexity measure"
       [F. Guidi: "Procedural Representation of CIC Proof Terms"
       nodes are counted according to the "intrinsic complexity measure"
       [F. Guidi: "Procedural Representation of CIC Proof Terms"
-      Journal of Automated Reasoning 44(1-2), Springer (February 2010), pp. 53-78].       
+      Journal of Automated Reasoning 44(1-2), Springer (February 2010), pp. 53-78].
    </topitem>
    </topitem>
-   <topitem>
-      <notice class="alpha" notice="Notice on displayed logical structures:"/>
+   <topitem name="notice2">
+      <notice class="alpha" text="Notice on displayed logical structures:"/>
       from the logical standpoint, the source scripts are grouped in "planes"
       and these are grouped in "components";
       the notation for the relations or functions
       introduced in each script, is shown in parentheses (? are placeholders).
    </topitem>
 
       from the logical standpoint, the source scripts are grouped in "planes"
       and these are grouped in "components";
       the notation for the relations or functions
       introduced in each script, is shown in parentheses (? are placeholders).
    </topitem>
 
+<!-- VERSION 3 =========================================================== -->
+
+   <subsection name="v3"><img logo="ld3"/>λδ version 3 (proposed)</subsection>
+   <body>
+      The formal specification of λδ version 3
+      is forthcoming.
+   </body>
+
 <!-- VERSION 2 =========================================================== -->
 
 <!-- VERSION 2 =========================================================== -->
 
-   <subsection name="v2"><version2-icon/>λδ version 2 (active)</subsection>
+   <subsection name="v2"><img logo="ld2"/>λδ version 2 (active)</subsection>
    <body>
       The formal specification of λδ version 2
    <body>
       The formal specification of λδ version 2
-      is available in the following formats:
+      is available in the following formats.
+   </body>
+
+   <body>
+      <notice class="alpha" text="Notice:"/>
+      the scripts are checked by the latest version of Matita from
+      <link to="http://matita.cs.unibo.it/gitweb/?p=helm.git;a=summary">HELM Git repository</link>.
    </body>
 
    </body>
 
-   <topitem name="source2">
+   <topitem name="source2B">
       <body>
       <body>
-         <rlink to="download/lambdadelta_2A1.tar.gz">lambdadelta_2A1 for Matita 0.99.2</rlink>
-         (revised <notice class="gamma" notice="2014-10"/>).
+         <rlink to="download/lambdadelta_2B.tar.bz2">lambdadelta_2B for Matita 0.99.4</rlink>
+         (revised <notice class="gamma" text="2020-12"/>).
          Source scripts.
          Source scripts.
-         <rlink to="documentation.html#ldR2c">Documentation (R2c)</rlink>.
+         <rlink to="html/documentation.html#ldJ2a">Documentation (J2a)</rlink>.
+         <list><item>
+            <notice class="gamma" text="2020-12-08."/>
+            repackaged for publication [Git revision: 2020-12-08 19:00:50].
+         </item><item>
+            <notice class="gamma" text="2020-02-27."/>
+            repackaged without λδ-ground [Git revision: 2020-02-27 22:45:50].
+         </item><item>
+            <notice class="gamma" text="2019-11-19."/>
+            released [Git revision: 2019-11-19 20:45:15].
+         </item></list>
       </body>
       <body>
       </body>
       <body>
-         The scripts are grouped in directories, first by part, then by component.
+         The scriprs depend on the package
+         <rlink to="html/specification.html#source2g">lambdadelta_ground</rlink>.
       </body>
       <body>
       </body>
       <body>
-         <notice class="alpha" notice="Notice:"/>
-         the scripts are checked by the latest version of Matita from
-         <link to="http://matita.cs.unibo.it/download.shtml">HELM Subversion repository</link>
-         at path &lt;trunk/matita/&gt;.
+         Informational pages on the parts of the specification:
+         <rlink to="html/static_2.html">Syntax</rlink>,
+         <rlink to="html/basic_2.html">Core</rlink>,
+         <rlink to="html/apps_2.html">Applications</rlink>.
+   </body>
+   </topitem>
+
+   <topitem name="source2A">
+      <body>
+         <rlink to="download/lambdadelta_2A.tar.bz2">lambdadelta_2A for Matita 0.99.2</rlink>
+         (revised <notice class="delta" text="2020-02"/>).
+         Source scripts.
+         <rlink to="html/documentation.html#ldR2c">Documentation (R2c)</rlink>.
+         <list><item>
+            <notice class="delta" text="2020-02-27."/>
+            repackaged on the basis of λδ-ground [Git revision: 2020-02-27 22:45:50].
+         </item><item>
+            <notice class="delta" text="2019-11-20."/>
+            repackaged (was lambdadelta_2A1) [Git revision: 2019-11-20 19:08:07].
+         </item><item>
+            <notice class="gamma" text="2014-10-28."/>
+            released [Git revision: 2014-10-28 17:46:26].
+         </item></list>
+      </body>
+      <body>
+         The scriprs depend on the package
+         <rlink to="html/specification.html#source2g">lambdadelta_ground</rlink>.
+      </body>
+      <body>
+         Informational pages on the parts of the specification:
+         <rlink to="html/basic_2A.html">Core</rlink>.
       </body>
    </topitem>
 
       </body>
    </topitem>
 
-   <body>
-      Informational pages on the parts of the specification:
-      <rlink to="ground_2.html">Background</rlink>,
-      <rlink to="basic_2.html">Core</rlink>,
-      <rlink to="apps_2.html">Applications</rlink>.
-   </body>
+   <topitem name="source2g">
+      <body>
+         <rlink to="download/lambdadelta_ground.tar.bz2">lambdadelta_ground for Matita 0.99.2</rlink>
+         (revised <notice class="gamma" text="2020-12"/>).
+         Source scripts.
+         <list><item>
+            <notice class="gamma" text="2020-12-08."/>
+            repackaged for publication [Git revision: 2020-12-08 19:00:50].
+         </item><item>
+            <notice class="gamma" text="2020-02-27."/>
+            released [Git revision: 2020-02-27 22:45:50].
+         </item></list>
+      </body>
+      <body>
+         Informational pages on the parts of the specification:
+         <rlink to="html/ground.html">Core</rlink>.
+      </body>
+   </topitem>
 
 <!-- VERSION 1 =========================================================== -->
 
 
 <!-- VERSION 1 =========================================================== -->
 
-   <subsection name="v1"><version1-icon/>λδ version 1 (superseded)</subsection>
+   <subsection name="v1"><img logo="ld1"/>λδ version 1 (superseded)</subsection>
    <body>
       The formal specification of λδ version 1
    <body>
       The formal specification of λδ version 1
-      is available in the following formats:
+      is available in the following formats.
    </body>
 
    </body>
 
-   <topitem name="source1">
+   <topitem name="source1A">
       <body>
       <body>
-         <rlink to="download/lambdadelta_1.tar.gz">lambdadelta_1 for Coq 7.3.1</rlink>
-         (revised <notice class="delta" notice="2015-09"/>).
+         <rlink to="download/lambdadelta_1A.tar.bz2">lambdadelta_1A for Coq 7.3.1</rlink>
+         (revised <notice class="delta" text="2019-11"/>).
          Source scripts.
          Source scripts.
-         <rlink to="documentation.html#ldJ1a">Documentation (J1a)</rlink>.
+         <rlink to="html/documentation.html#ldJ1a">Documentation (J1a)</rlink>.
          <list><item>
          <list><item>
-            <notice class="delta" notice="2015 January 15."/>
+            <notice class="delta" text="2019-11-20."/>
+            repackaging (was lambdadelta_1) [Git revision: 2019-11-20 19:08:07].
+         </item><item>
+            <notice class="delta" text="2015-01-15."/>
             17 new lemmas and former lemma "eq_nat_dec" renamed as "nat_dec_neg".
          </item></list>
             17 new lemmas and former lemma "eq_nat_dec" renamed as "nat_dec_neg".
          </item></list>
-      </body>      
+      </body>
       <body>
       <body>
-         The scripts are grouped in directories, one for each part.
+         Informational pages on the parts of the specification:
+         <rlink to="html/ground_1.html">Background</rlink>,
+         <rlink to="html/basic_1.html">Core</rlink>.
       </body>
    </topitem>
 
       </body>
    </topitem>
 
-   <topitem name="static1">
-      <rlink to="static/matita/lambdadelta/">lambdadelta_1 for Matita 0.5</rlink>
-      (revised <notice class="delta" notice="2011-09"/>).
-      Static HTML pages generated by the <link to="http://helm.cs.unibo.it/">HELM</link> rendering engine.  
+   <topitem name="static1A">
+      <rlink to="static/matita/lambdadelta/">lambdadelta_1A for Matita 0.5</rlink>
+      (revised <notice class="delta" text="2019-11"/>).
+      Static HTML pages generated by the <link to="http://helm.cs.unibo.it/">HELM</link> rendering engine.
       <list><item>
          <rlink to="static/matita/lambdadelta/basic_1/pr3/pr3/pr3_confluence.con.html">
             Confluence of reduction</rlink>
       <list><item>
          <rlink to="static/matita/lambdadelta/basic_1/pr3/pr3/pr3_confluence.con.html">
             Confluence of reduction</rlink>
@@ -128,19 +203,13 @@
       </item></list>
    </topitem>
 
       </item></list>
    </topitem>
 
-   <topitem name="dynamic1">
+   <topitem name="dynamic1A">
       <link to="http://mowgli.cs.unibo.it:58080/apply?keys=RT&amp;xmluri=http://helm.cs.unibo.it/helm//html/folder/index.html&amp;prop.media-type=text/html&amp;param.thmedia-type=text/html&amp;param.thkeys=T1%2CT2%2CL%2CE&amp;param.embedkeys=d_c%2CTC1%2CHC2%2CL&amp;param.thencoding=UTF-8&amp;prop.encoding=UTF-8&amp;prop.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&amp;param.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&amp;param.encoding=UTF-8&amp;param.media-type=text/html&amp;param.keys=d_c%2CC1%2CHC2%2CL&amp;profile=default&amp;param.profile=default&amp;param.CICURI=theory:/matita/lambdadelta/">
       <link to="http://mowgli.cs.unibo.it:58080/apply?keys=RT&amp;xmluri=http://helm.cs.unibo.it/helm//html/folder/index.html&amp;prop.media-type=text/html&amp;param.thmedia-type=text/html&amp;param.thkeys=T1%2CT2%2CL%2CE&amp;param.embedkeys=d_c%2CTC1%2CHC2%2CL&amp;param.thencoding=UTF-8&amp;prop.encoding=UTF-8&amp;prop.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&amp;param.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&amp;param.encoding=UTF-8&amp;param.media-type=text/html&amp;param.keys=d_c%2CC1%2CHC2%2CL&amp;profile=default&amp;param.profile=default&amp;param.CICURI=theory:/matita/lambdadelta/">
-         lambdadelta_1 for Matita 0.5</link>
-      (revised <notice class="delta" notice="2011-09"/>).
+         lambdadelta_1A for Matita 0.5</link>
+      (revised <notice class="delta" text="2019-11"/>).
       <link to="http://helm.cs.unibo.it/">HELM</link> directory.
       <link to="http://helm.cs.unibo.it/">HELM</link> directory.
-      <notice class="alpha" notice="Notice: the HELM rendering engine is offline."/>
+      <notice class="alpha" text="Notice: the HELM rendering engine is offline."/>
    </topitem>
 
    </topitem>
 
-   <body>
-      Informational pages on the parts of the specification:
-      <rlink to="ground_1.html">Background</rlink>,
-      <rlink to="basic_1.html">Core</rlink>.
-   </body>
-
    <footer/>
 </page>
    <footer/>
 </page>
Unnamed repository; edit this file 'description' to name the repository.