]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/www/lambdadelta/index.html
mailstone in basic_2 !! "big tree" theorem completed after 15 months
[helm.git] / helm / www / lambdadelta / index.html
index a224e9df64e98e310fb71ab57688f03e96a3eb83..07e98c6a926e9ec182be6d56c1ff5853404fd173 100644 (file)
@@ -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">
@@ -9,7 +10,7 @@
   <link rel="shortcut icon" href="images/crux_16.ico"></head><body>
 <div style="text-align: center;">
 <br>
-<a href="http://lambdadelta.info"><img alt="[Crux Logo]" title="The Crux" src="images/crux_32.png" style="border: 0px solid ; width: 32px; height: 32px;"></a>
+<a href="http://lambdadelta.info/"><img alt="[Crux Logo]" title="The Crux" src="images/crux_32.png" style="border: 0px solid ; width: 32px; height: 32px;"></a>
 <h1>The Formal System λδ (\lambda\delta)<br>
 </h1>
 <h2>Towards the unification of terms, types, environments and contexts</h2>
@@ -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
@@ -91,7 +92,7 @@ includes the major milestones:<br>
             </td>
             <td style="vertical-align: top; background-color: rgb(255, 223, 191);">planned
 in
-2013<br>
+2014<br>
             </td>
             <td style="vertical-align: top; background-color: rgb(255, 223, 191);">not
 planned yet<br>
@@ -137,8 +138,8 @@ 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 2014-02-24 by <a href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
 Guidi</a><br>
 </div>
 
-</body></html>
\ No newline at end of file
+</body></html>