]> 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
update in binararies for λδ
[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 556549c393d00f5190ddc0d40f9f3c4440c27379..050a17328536089873fad5eb223d134d6a70351c 100644 (file)
--- a/helm/www/lambdadelta/web/home/specification.ldw.xml
+++ b/helm/www/lambdadelta/web/home/specification.ldw.xml
@@ -3,107 +3,178 @@
 <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"/>
 
-   <section5 name="specifications">Computer-checked formal specifications</section5>
+   <section15 name="specifications">Computer-checked formal specifications</section15>
    <body>
    <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_2.tar.gz">lambdadelta_2 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-02"/>).
          Source scripts.
          Source scripts.
+         <rlink to="html/documentation.html#ldJ2a">Documentation (J2a)</rlink>.
+         <list><item>
+            <notice class="gamma" text="2020-02-27."/>
+            repackaged without λδ-ground_2.
+         </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_2.
+         </item><item>
+            <notice class="delta" text="2019-11-20."/>
+            repackaged (was lambdadelta_2A1).
+         </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-02"/>).
+         Source scripts.
+         <list><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_2.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-01"/>).
+         <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="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).
+         </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>
@@ -126,19 +197,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.