X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Flibrary.shtml;h=3c4246f313b566485c3bf0ec9180281e0221b06b;hb=3cb42e0873c101c6c5a8b9967d765b5135882685;hp=c22db5e1ce9f03802dcbcb812811ff85175bef68;hpb=ecf6f2741d56261acf4580379d35117d80385da2;p=helm.git

diff --git a/helm/www/matita/library.shtml b/helm/www/matita/library.shtml
index c22db5e1c..3c4246f31 100644
--- a/helm/www/matita/library.shtml
+++ b/helm/www/matita/library.shtml
@@ -59,8 +59,30 @@
       </p>
 
       <h2>The Formal System &lambda;&delta; (lambda-delta)<a name="lambda-delta"></a></h2>
+      
+      <p>The formal system &lambda;&delta; is a typed &lambda;-calculus that
+         pursues the unification of terms, types, environments and contexts
+	 as the main goal.
+         &lambda;&delta; takes some features from the Automath-related
+	 &lambda;-calculi and some from the pure type systems, but differs
+	 from both in that it does not include the &Pi; construction while it
+	 provides for an abbreviation mechanism at the level of terms.
+      </p>
+
+      <p> The development presents the proofs of some important properties that
+          &lambda;&delta; enjoys. In particular: 
+          <ul> <li> the confluence of reduction </li>
+               <li> the correctness of types </li>
+               <li> the uniqueness of types up to conversion </li>
+               <li> the subject reduction of the type assignment </li>
+               <li> the strong normalization of the typed terms </li>
+               <li> the decidability of type inference problem </li>
+          </ul>
+      </p>
+      
       <p>
-      See the <a href="http://helm.cs.unibo.it/lambda-delta/">&lambda;&delta; home page</a>.
+       See the <a href="http://helm.cs.unibo.it/lambda-delta/">&lambda;&delta; home page</a>
+       for more information.
       </p>
 
       <!--#include virtual="bottombar.shtml" -->