...

[helm.git] / helm / www / matita / library.shtml
diff --git a/helm/www/matita/library.shtml b/helm/www/matita/library.shtml

index a6f195b630f6c9f6eed33b9df899c8323de49fee..3c4246f313b566485c3bf0ec9180281e0221b06b 100644 (file)
--- a/helm/www/matita/library.shtml
+++ b/helm/www/matita/library.shtml
@@ -1,6 +1,6 @@
-<!-- $Id$ -->
  <!--#include virtual="xhtml-header.shtml" -->
-<html>
+<!-- $Id$ -->
+<html xmlns="http://www.w3.org/1999/xhtml">
    <head>
      <title>Matita - Library</title>
      <!--#include virtual="xhtml-meta.shtml" -->
@@ -29,14 +29,14 @@
         <li>an executable formalization of the operational semantics of
             any <a href="http://www.freescale.com">Freescale</a>
             micro-controller of the <a href="http://www.freescale.com/webapp/sps/site/homepage.jsp?nodeId=0162468449&tid=FSH">HC05/HC08/RS08/HCS08 families</a>
+           </li>
         <li>a compiler from assembly language (pseudocodes + operands) to
-           machine code
+       machine code</li>
         <li>several automatic checks for unhandled opcodes, memory accesses,
-           correctness of ALU logic, etc.
+       correctness of ALU logic, etc.</li>
         <li>three examples of assembly programs (string reverse, counting sort
-           and perfect numbers sieve) with sets of data to run them
+       and perfect numbers sieve) with sets of data to run them</li>
        </ul>
-      </a>
        
        <p>The execution in the executable formalization has been compared
           to real world execution using the <a href="http://www.freescale.com/webapp/sps/site/overview.jsp?code=784_LPBBNEWTOOL&fsrch=1">USB SPYDER08</a>
@@ -58,6 +58,33 @@
           here</a>.
        </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>
+       for more information.
+      </p>
+
        <!--#include virtual="bottombar.shtml" -->
      </div>
    </body>