]> matita.cs.unibo.it Git - helm.git/commitdiff
projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: c259a5f)
some corrections to the prose of the web site
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Sun, 2 Dec 2012 12:28:43 +0000 (12:28 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Sun, 2 Dec 2012 12:28:43 +0000 (12:28 +0000)
helm/www/lambdadelta/documentation.html patch | blob | history
helm/www/lambdadelta/implementation.html patch | blob | history
helm/www/lambdadelta/index.html patch | blob | history
helm/www/lambdadelta/news.html patch | blob | history

diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html
index 0bb864a9cbf5e62fb94aea5402a7faf390ac04bd..425084d70d3e30bd4b65168a54c8feb9fedcfd99 100644 (file)
--- a/helm/www/lambdadelta/documentation.html
+++ b/helm/www/lambdadelta/documentation.html
@@ -1,6 +1,7 @@
 <!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
 <html dir="ltr" lang="en-us"><head>
 
+
   
     <meta content="text/html; charset=UTF-8" http-equiv="content-type"><title>λδ home page</title>
     
@@ -38,7 +39,7 @@
               Currently the <span style="font-weight: bold;">main
                 source of
                 information</span> on λδ (version 1) is <span style="font-weight: bold;">Resource
-                1.1</span> below.<br>
+                1.9</span> below.<br>
               A <span style="font-weight: bold;">summary</span> of
               basic λδ (version
               1) is found in <span style="font-weight: bold;">Resource
@@ -50,7 +51,7 @@
               <table style="text-align: left; width: 100%;" border="0" cellpadding="2" cellspacing="2">
                 <tbody>
                   <tr>
-                    <td style="vertical-align: top;">2.1.<br>
+                    <td style="vertical-align: top;">2.4.<br>
                     </td>
                     <td style="vertical-align: top;"><a name="ldp7"></a>F.
                       Guidi: <a href="download/cie_2010.pdf"><span style="font-style: italic;">An
@@ -65,7 +66,7 @@
                     </td>
                   </tr>
                   <tr>
-                    <td style="vertical-align: top;">2.2.<br>
+                    <td style="vertical-align: top;">2.3.<br>
                     </td>
                     <td style="vertical-align: top;"> <a name="ldp6"></a>F.
 Guidi:
@@ -89,7 +90,7 @@ Guidi:
                     </td>
                   </tr>
                   <tr>
-                    <td style="vertical-align: top;">2.3.<br>
+                    <td style="vertical-align: top;">2.2.<br>
                     </td>
                     <td style="vertical-align: top;"><a name="ldt7"></a>F.
                       Guidi: <a href="download/ld_talk_7s.pdf"><span style="font-style: italic;">An
@@ -105,7 +106,7 @@ Guidi:
                     </td>
                   </tr>
                   <tr>
-                    <td style="vertical-align: top;">2.4.<br>
+                    <td style="vertical-align: top;">2.1.<br>
                     </td>
                     <td style="vertical-align: top;"><a name="ldt6"></a>F.
                       Guidi: <a href="download/ld_talk_6s.pdf"><span style="font-style: italic;">A
@@ -127,7 +128,7 @@ Guidi:
               <table style="text-align: left; width: 100%;" border="0" cellpadding="2" cellspacing="2">
                 <tbody>
                   <tr>
-                    <td style="vertical-align: top;">1.1.<br>
+                    <td style="vertical-align: top;">1.9.<br>
                     </td>
                     <td style="vertical-align: top;"><a name="ldp5"></a>F.
 Guidi:
@@ -145,7 +146,7 @@ Guidi:
                     </td>
                   </tr>
                   <tr>
-                    <td style="vertical-align: top;">1.2.<br>
+                    <td style="vertical-align: top;">1.8.<br>
                     </td>
                     <td style="vertical-align: top;"><a name="ldp4"></a>F.
                       Guidi: <a href="download/cie_2007.pdf"><span style="font-style: italic;">Lambda
@@ -170,7 +171,7 @@ Guidi:
                     </td>
                   </tr>
                   <tr>
-                    <td style="vertical-align: top;">1.3.<br>
+                    <td style="vertical-align: top;">1.7.<br>
                     </td>
                     <td style="vertical-align: top;"><a name="ldp3"></a>F.
                       Guidi: <a href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2006.bib?ncstrl.cabernet//BOLOGNA-UBLCS-2006-25"><span style="font-style: italic;">Lambda Types on
@@ -187,7 +188,7 @@ Guidi:
                     </td>
                   </tr>
                   <tr>
-                    <td style="vertical-align: top;">1.4.<br>
+                    <td style="vertical-align: top;">1.6.<br>
                     </td>
                     <td style="vertical-align: top;"><a name="ldp2"></a>F.
                       Guidi: <a style="font-style: italic;" href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2006.bib?ncstrl.cabernet//BOLOGNA-UBLCS-2006-01">Lambda
@@ -212,7 +213,7 @@ Guidi:
                     <td style="vertical-align: top;"><a name="ldt5"></a>F.
                       Guidi: <a style="font-style: italic;" href="download/ld_talk_5s.pdf">The
                         Formal
-                        System lambdadelta</a>
+                        System </a><a href="download/cie_2010.pdf"><span style="font-style: italic;">λδ</span></a>
                       (<span style="font-weight: bold;">2008-10</span>).
                       Presentation at
                       "Advances in Constructive Topology and Logical
@@ -221,7 +222,7 @@ Guidi:
                     </td>
                   </tr>
                   <tr>
-                    <td style="vertical-align: top;">1.6.<br>
+                    <td style="vertical-align: top;">1.4.<br>
                     </td>
                     <td style="vertical-align: top;"><a name="ldt4"></a>F.
                       Guidi: <a href="download/ld_talk_4s.pdf"><span style="font-style: italic;">Towards
@@ -236,7 +237,7 @@ Guidi:
                     </td>
                   </tr>
                   <tr>
-                    <td style="vertical-align: top;">1.7.<br>
+                    <td style="vertical-align: top;">1.3.<br>
                     </td>
                     <td style="vertical-align: top;"><a name="ldt3"></a>F.
                       Guidi: <a href="download/ld_talk_3s.pdf"><span style="font-style: italic;">Lambda
@@ -251,7 +252,7 @@ Guidi:
                     </td>
                   </tr>
                   <tr>
-                    <td style="vertical-align: top;">1.8.<br>
+                    <td style="vertical-align: top;">1.2.<br>
                     </td>
                     <td style="vertical-align: top;"><a name="ldt2"></a>F.
                       Guidi: <a href="download/ld_talk_2s.pdf"><span style="font-style: italic;">Lambda
@@ -269,7 +270,7 @@ Guidi:
                     </td>
                   </tr>
                   <tr>
-                    <td style="vertical-align: top;">1.9.<br>
+                    <td style="vertical-align: top;">1.1.<br>
                     </td>
                     <td style="vertical-align: top;"><a name="ldt1"></a>F.
 Guidi:
@@ -291,10 +292,11 @@ Guidi:
       <br>
       <a href="http://validator.w3.org/check?uri=referer"><img alt="[Valid HTML 4.01 Transitional]" title="Valid HTML 4.01
           Transitional" src="http://www.w3.org/Icons/valid-html401" style="border: 0px solid ; width: 88px; height: 31px;"></a> <a href="http://www.anybrowser.org/campaign/"><img alt="[Use Any
-          Browser Here]" title="Use Any Browser Here" src="images/globe_trans.png" style="border: 0px solid ; width: 147px; height: 42px;"></a> <img style="width: 88px; height: 31px;" alt="[PNG Used Here]" title="PNG Used Here]" src="http://www.cs.unibo.it/%7Efguidi/images/PNGnow2.png"><br>
+          Browser Here]" title="Use Any Browser Here" src="images/globe_trans.png" style="border: 0px solid ; width: 147px; height: 42px;"></a> <img style="width: 88px; height: 31px;" alt="[PNG Used Here]" title="PNG Used Here]" src="images/PNGnow2.png"><br>
       <br>
-      Last update 2012-12-01 by <a href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
+      Last update 2012-12-02 by <a href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
         Guidi</a><br>
     </div>
   
+
 </body></html>
\ No newline at end of file
diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html
index 0163d01c463fee47813a969058240e17d2d89fa8..e5ecc5760a941cabbf720cc6d11bf92fa3861f26 100644 (file)
--- a/helm/www/lambdadelta/implementation.html
+++ b/helm/www/lambdadelta/implementation.html
@@ -1,6 +1,7 @@
 <!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
 <html dir="ltr" lang="en-us"><head>
 
+
   
     <meta content="text/html; charset=UTF-8" http-equiv="content-type"><title>λδ home page</title>
     
@@ -106,7 +107,7 @@
                   <br>
                 </li>
                 <li><a name="ldp1"></a>F. Guidi: <a href="download/lambdadelta_1.tar.gz"><span style="font-style: italic;">lambdadelta_1</span></a>
-                  (revised <span style="font-weight: bold;">2011-09</span>).
+                  (revised <span style="font-weight: bold;">2012-10</span>).
 Formal
                   specification for <span style="font-weight: bold;">Coq
                     7.3.1</span>
@@ -129,8 +130,8 @@ Formal
                   <span style="font-weight: bold;"></span></li>
               </ul>
               <ul>
-                <li><span style="font-weight: bold;">Access:</span> <a href="static/lddl/">static pages</a> (updated <span style="font-weight: bold;">2011-09</span>), <a href="download/lddl.tar.bz2">data set</a> (updated <span style="font-weight: bold;">2011-09</span>), <a href="http://lambdadelta.info/xml">HELM server URL</a>
-                  (updated <span style="font-weight: bold;">2011-09</span>).</li>
+                <li><span style="font-weight: bold;">Access:</span> <a href="static/lddl/">static pages</a> (updated <span style="font-weight: bold;">2012-10</span>), <a href="download/lddl.tar.bz2">data set</a> (updated <span style="font-weight: bold;">2012-10</span>), <a href="http://lambdadelta.info/xml">HELM server URL</a>
+                  (updated <span style="font-weight: bold;">2012-10</span>).</li>
               </ul>
               <ul>
                 <li><span style="font-weight: bold;">Examples:</span> <a href="static/lddl/brg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">Grundlagen's
@@ -216,7 +217,7 @@ computer
                 <li><a name="bibtex"></a>A
                   BibTeX database of λδ documentation: <a href="download/lambdadelta.bib"><span style="font-style: italic;">lambdadelta.bib</span></a>,
                   <a style="font-style: italic;" href="download/lambdadelta.txt">lambdadelta.txt</a>
-                  (revised <span style="font-weight: bold;">2011-09</span>).</li>
+                  (revised <span style="font-weight: bold;">2012-10</span>).</li>
               </ul>
               <ul>
                 <li>A <a href="http://www.jedsoft.org/jed/">Jed mode</a>
@@ -245,7 +246,7 @@ computer
           Transitional" src="http://www.w3.org/Icons/valid-html401" style="border: 0px solid ; width: 88px; height: 31px;"></a> <a href="http://www.anybrowser.org/campaign/"><img alt="[Use Any
           Browser Here]" title="Use Any Browser Here" src="images/globe_trans.png" style="border: 0px solid ; width: 147px; height: 42px;"></a> <img style="width: 88px; height: 31px;" alt="[PNG Used Here]" title="PNG Used Here" src="images/PNGnow2.png"><br>
       <br>
-      Last update 2012-12-01 by <a href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
+      Last update 2012-12-02 by <a href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
         Guidi</a><br>
     </div>
   
diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html
index a224e9df64e98e310fb71ab57688f03e96a3eb83..45fd133bb1a66593e9a081bae4f4e70bee0844ad 100644 (file)
--- a/helm/www/lambdadelta/index.html
+++ b/helm/www/lambdadelta/index.html
@@ -2,6 +2,7 @@
 <html dir="ltr" lang="en-us"><head>
 
 
+
   <meta content="text/html; charset=UTF-8" http-equiv="content-type"><title>λδ home page</title>
   
   <meta content="Ferruccio Guidi" name="author">
@@ -37,7 +38,7 @@
 The formal system λδ
 (\lambda\delta) is a typed lambda calculus that pursues the static and
 dynamic unification of terms, types, environments and contexts while
-enjoying a well-conceived meta-theory, which includes the commonly
+enjoying a well-conceived theory, which includes the commonly
 desired properties.<br>
       <br>
 λδ takes some features from the calculi of the Automath family and
@@ -53,7 +54,7 @@ The reduction steps of λδ include β-contraction, δ-expansion,
 ζ-contraction and θ-swap. On the other hand,
 η-contraction is not included.<br>
       <br>
-The meta-theory of λδ includes important properties such as the
+The theory of λδ includes important properties such as the
 confluence of reduction, the correctness of types, the
 uniqueness of types up to conversion, the subject reduction of the type
 assignment, the strong normalization of the typed terms. The
@@ -137,7 +138,7 @@ Options" entry → "General" tab → "Fonts" button.</span><br>
 <br>
 <a href="http://validator.w3.org/check?uri=referer"><img alt="[Valid HTML 4.01 Transitional]" title="Valid HTML 4.01 Transitional" src="http://www.w3.org/Icons/valid-html401" style="border: 0px solid ; width: 88px; height: 31px;"></a> <a href="http://www.anybrowser.org/campaign/"><img alt="[Use Any Browser Here]" title="Use Any Browser Here" src="images/globe_trans.png" style="border: 0px solid ; width: 147px; height: 42px;"></a> <img style="width: 88px; height: 31px;" alt="[PNG Used Here]" title="PNG Used Here" src="images/PNGnow2.png"><br>
 <br>
-Last update 2012-12-01 by <a href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
+Last update 2012-12-02 by <a href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
 Guidi</a><br>
 </div>
 
diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html
index 8ca8c771df44b58ee8ebf7bd778e92582e157b1e..1c20541234bf5164386993f72a0213a7e867606f 100644 (file)
--- a/helm/www/lambdadelta/news.html
+++ b/helm/www/lambdadelta/news.html
@@ -2,6 +2,7 @@
 <html dir="ltr" lang="en-us"><head>
 
 
+
   <meta content="text/html; charset=UTF-8" http-equiv="content-type"><title>λδ home page</title>
   
   <meta content="Ferruccio Guidi" name="author">
@@ -115,7 +116,7 @@ for <a href="http://matita.cs.unibo.it/">Matita 0.5</a> of the <a href="implemen
       </ul>
       <ul>
         <li><span style="font-weight: bold;">May 2008.</span> The
-specification of λδ version 1 is closed.<br>
+specification of λδ version 1 is dismissed.<br>
           <span style="font-weight: bold;"></span></li>
       </ul>
       <ul>
@@ -224,7 +225,7 @@ this site as the first result.</li>
           Transitional" src="http://www.w3.org/Icons/valid-html401" style="border: 0px solid ; width: 88px; height: 31px;"></a> <a href="http://www.anybrowser.org/campaign/"><img alt="[Use Any
           Browser Here]" title="Use Any Browser Here" src="images/globe_trans.png" style="border: 0px solid ; width: 147px; height: 42px;"></a> <img style="width: 88px; height: 31px;" alt="[PNG Used Here]" title="PNG Used Here" src="images/PNGnow2.png"><br>
 <br>
-Last update 2012-12-01 by <a href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
+Last update 2012-12-02 by <a href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
 
 Guidi</a><br>
 </div>
Unnamed repository; edit this file 'description' to name the repository.