helm/www/lambda_delta/news.html

   1 <!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
   2 <html>
   3   <head>
   4     <meta content="text/html; charset=UTF-8" http-equiv="content-type">
   5     <title>lambda_delta home page</title>
   6     <meta content="Ferruccio Guidi" name="author">
   7     <meta content="The formal system lambda_delta" name="description">
   8     <link rel="shortcut icon" href="download/crux_16.ico">
   9   </head>
  10   <body>
  11     <div style="text-align: center;">
  12       <br>
  13       <a href="http://lambda-delta.info"><img alt="[Crux Logo]"
  14           title="The Crux" src="download/crux_32.png" style="border: 0px
  15           solid ; width: 32px; height: 32px;"></a>
  16       <h1>The Formal System λδ (lambda_delta)<br>
  17       </h1>
  18       <h2>Towards the unification of terms, types, environments and
  19         contexts</h2>
  20       <img style="width: 95%; height: 4px;" alt="[Separator]"
  21         title="Separator" src="download/rainbow.png"><br>
  22       <table style="text-align: left; width: 95%; margin-left: auto;
  23         margin-right: auto;" border="0" cellpadding="2" cellspacing="20">
  24         <tbody>
  25           <tr>
  26             <td style="vertical-align: top;">
  27               <ul>
  28                 <li><a href="index.html">Foreword</a></li>
  29               </ul>
  30               <ul>
  31                 <li>News</li>
  32               </ul>
  33               <ul>
  34                 <li><a href="documentation.html">Papers</a></li>
  35               </ul>
  36               <ul>
  37                 <li><a href="implementation.html">Resources</a><br>
  38                 </li>
  39               </ul>
  40             </td>
  41             <td style="vertical-align: top; text-align: left;">
  42               <h3 style="text-align: right;">News <img style="width:
  43                   37px; height: 37px;" alt="[Butterfly]"
  44                   title="Butterfly" src="download/b5.png"></h3>
  45               <ul>
  46                 <li><span style="font-weight: bold;">September 2011.</span>
  47                   The
  48                   denomination "lambda-delta" changes to "lambda_delta".
  49                 <ul>
  50                   <li>The character "-" is reserved in λδ textual syntax
  51                     (recognized by <span style="font-style: italic;">Helena
  52                       0.8.1</span>).
  53                   </li>
  54                   <li>Eventually, the occurrences of the character "-"
  55                     will be
  56                     replaced by "_" in all λδ-related identifiers.</li>
  57                   <li>In particular, this refactoring involves file
  58                     names and
  59                     path names.</li>
  60                   <li>The permanent λδ URL is sheduled to become <span
  61                       style="font-style: italic;">http://lambda_delta.info</span>
  62                     on
  63                     December 2012.<br>
  64                   </li>
  65                 </ul></li>
  66               </ul>
  67               <ul>
  68                 <li><span style="font-weight: bold;">April 2011.</span>
  69                   The
  70                   specification of λδ version 2 and related topics is
  71                   restarted in <a href="http://matita.cs.unibo.it/">Matita
  72                     0.5</a>.
  73                 <ul>
  74                   <li><a href="apps_2.html">Here</a> is a page about
  75                     the
  76                     topics related to the specification (Applications).</li>
  77                   <li><a href="basic_2.html">Here</a> is a page about
  78                     the
  79                     specification (Core).
  80                   </li>
  81                 </ul></li>
  82               </ul>
  83               <ul>
  84                 <li><span style="font-weight: bold;">December 2010.</span>
  85                   Permanent λδ URL acquired: <a
  86                     href="http://lambda-delta.info">http://lambda-delta.info</a>
  87                   (pointing at this site). <br>
  88                   <span style="font-weight: bold;"></span></li>
  89               </ul>
  90               <ul>
  91                 <li><span style="font-weight: bold;">November 2010.</span>
  92                   <span style="font-style: italic;">Helena 0.8.1</span>
  93                   is released. <br>
  94                 </li>
  95               </ul>
  96               <ul>
  97                 <li><span style="font-weight: bold;">September 2009.</span>
  98                   <span style="font-style: italic;">Helena 0.8.0</span>
  99                   is released and the <a
 100                     href="implementation.html#lddl">λδ Digital Library</a>
 101                   is
 102                   started.<br>
 103                   <span style="font-weight: bold;"></span></li>
 104               </ul>
 105               <ul>
 106                 <li><span style="font-weight: bold;">June 2009.</span> <span
 107                     style="font-style: italic;">Helena</span>, a <a
 108                     href="implementation.html#helena">validator for λδ
 109                     version 2</a>, is
 110                   available
 111                   as
 112                   a
 113                   part
 114                   of
 115                   the <a href="http://helm.cs.unibo.it/">HELM</a>
 116                   software. <br>
 117                 </li>
 118               </ul>
 119               <span style="font-weight: bold;"></span>
 120               <ul>
 121                 <li><span style="font-weight: bold;">September 2008.</span>
 122                   This site is online.<br>
 123                 </li>
 124               </ul>
 125               <span style="font-weight: bold;"></span>
 126               <ul>
 127                 <li><span style="font-weight: bold;">July 2008.</span> <a
 128                     href="documentation.html#ldp5">First journal paper
 129                     on λδ</a> accepted
 130                   for publication.</li>
 131               </ul>
 132               <ul>
 133                 <li><span style="font-weight: bold;">July 2008.</span>
 134                   First <a href="http://helm.cs.unibo.it/procedural/">procedural
 135                     reconstruction</a> for <a
 136                     href="http://matita.cs.unibo.it/">Matita 0.5</a>
 137                   of the <a href="implementation.html#ldp1">λδ proof
 138                     scripts for
 139                     Coq 7.3.1</a>.<br>
 140                 </li>
 141               </ul>
 142               <ul>
 143                 <li><span style="font-weight: bold;">June 2008.</span>
 144                   The <a href="implementation.html#static">HTML
 145                     pages of the specification of λδ version 1 for
 146                     Matita 0.5</a> are
 147                   online.<br>
 148                   <span style="font-weight: bold;"></span></li>
 149               </ul>
 150               <ul>
 151                 <li><span style="font-weight: bold;">March 2008.</span>
 152                   The
 153                   specification of λδ version 2 is started with Coq
 154                   7.3.1 (false start).
 155                   <!--          <ul>
 156             <li>native type assignment with new rules for application: <span
 157  style="font-style: italic;">nty</span> (it replaces <span
 158  style="font-style: italic;">ty3</span>);<br>
 159             </li>
 160             <li>parallel conversion on focalized terms: <span
 161  style="font-style: italic;">fpcs</span> (it replaces <span
 162  style="font-style: italic;"></span><span style="font-style: italic;">pc3</span>);
 163               <br>
 164             </li>
 165             <li>new weak parallel reduction on environments: <span
 166  style="font-style: italic;">wcpr</span> <span
 167  style="font-style: italic;"></span>(it is based on <span
 168  style="font-style: italic;">fpr</span> and replaces <span
 169  style="font-style: italic;">wcpr0</span>);&nbsp; <br>
 170             </li>
 171             <li>parallel reduction on focalized terms: <span
 172  style="font-style: italic;">fpr</span> and <span
 173  style="font-style: italic;">fprs</span> (they replace <span
 174  style="font-style: italic;"></span><span style="font-style: italic;"></span><span
 175  style="font-style: italic;">pr2</span>, <span
 176  style="font-style: italic;">pr3</span>); <br>
 177             </li>
 178           </ul>
 179           <ul>
 180             <li>new thinning relation: <span
 181  style="font-style: italic;">drop</span>
 182 (it replaces the old <span style="font-style: italic;">drop</span>, <span
 183  style="font-style: italic;">clear</span>, <span
 184  style="font-style: italic;">getl</span>, <span
 185  style="font-style: italic;">cimp</span>, <span
 186  style="font-style: italic;">drop1</span>);</li>
 187             <li>new shift function: <span style="font-style: italic;">shift</span>:
 188 (it
 189 replaces
 190
 191               <span style="font-style: italic;">app1</span>);</li>
 192             <li>new length function for environments: <span
 193  style="font-style: italic;">clen</span>;<br>
 194             </li>
 195             <li>new relocation function: <span
 196  style="font-style: italic;">lift</span> (it replaces old <span
 197  style="font-style: italic;">lift</span>, <span
 198  style="font-style: italic;">lift1</span>);<br>
 199             </li>
 200             <li>new term structure with polarity indicators and no
 201 distinction between binding and flat items;</li>
 202             <li>new general theory of relocation (comprises new
 203 relocation functions: <span style="font-style: italic;">s</span>, <span
 204  style="font-style: italic;">r</span>);</li>
 205             <li>we removed context-free reduction and conversion (<span
 206  style="font-style: italic;">pr0</span>, <span
 207  style="font-style: italic;">pr1</span>, <span
 208  style="font-style: italic;">pc1</span>);<br>
 209             </li>
 210             <li>we removed greedy substitution (<span
 211  style="font-style: italic;"></span><span style="font-style: italic;">csubst0</span>,
 212               <span style="font-style: italic;">csubst1</span>, <span
 213  style="font-style: italic;">fsubst0</span>, <span
 214  style="font-style: italic;">subst0</span>, <span
 215  style="font-style: italic;">subst1</span>);<br>
 216             </li>
 217             <li>we removed level indicators on environments (<span
 218  style="font-style: italic;">cbk</span>).</li>
 219           </ul>
 220 --> </li>
 221               </ul>
 222               <ul>
 223                 <li><span style="font-weight: bold;">September 2007.</span>
 224                   The <a href="implementation.html#dynamic">specification
 225                     of λδ version
 226                     1 for
 227                     Matita 0.4</a> is online.</li>
 228               </ul>
 229               <ul>
 230                 <li><span style="font-weight: bold;">November 2006.</span>
 231                   <a href="documentation.html#ldp3">λδ version
 232                     1</a> is released.</li>
 233               </ul>
 234               <ul>
 235                 <li><span style="font-weight: bold;">December 2005.</span>
 236                   <a href="documentation.html#ldt1">First communication
 237                     on λδ</a>.<br>
 238                 </li>
 239               </ul>
 240               <ul>
 241                 <li><span style="font-weight: bold;">May 2004.</span>
 242                   The <a href="implementation.html#ldp1">specification
 243                     of λδ version 1</a> is
 244                   started with Coq 7.3.1.<br>
 245                 </li>
 246               </ul>
 247               <h3 style="text-align: right;">Visibility <img
 248                   style="width: 37px; height: 37px;" alt="[Butterfly]"
 249                   title="Butterfly" src="download/b4.png"></h3>
 250               <ul>
 251                 <li><span style="font-weight: bold;">February 2012.</span>
 252                   The <a href="http://www.google.com/">Google</a>
 253                   search for <span style="color: rgb(255, 0, 0);">formal
 254                     system lambda
 255                     delta</span>
 256                   gives 5 resources about λδ in the first 6 results.<br>
 257                 </li>
 258               </ul>
 259               <ul>
 260                 <li><span style="font-weight: bold;">February 2012.</span>
 261                   The <a href="http://www.yahoo.com/">Yahoo</a>
 262                   search <span style="color: rgb(255, 0, 0);">formal
 263                     system lambda delta</span>
 264                   gives this site as the first result.</li>
 265               </ul>
 266             </td>
 267           </tr>
 268         </tbody>
 269       </table>
 270       <br>
 271       <a href="http://validator.w3.org/check?uri=referer"><img
 272           alt="[Valid HTML 4.01 Transitional]" title="Valid HTML 4.01
 273           Transitional" src="http://www.w3.org/Icons/valid-html401"
 274           style="border: 0px solid ; width: 88px; height: 31px;"></a> <a
 275         href="http://www.anybrowser.org/campaign/"><img alt="[Use Any
 276           Browser Here]" title="Use Any Browser Here"
 277           src="download/globe_trans.png" style="border: 0px solid ;
 278           width: 147px; height: 42px;"></a> <img style="width: 88px;
 279         height: 31px;" alt="[PNG Used Here]" title="PNG Used Here"
 280         src="download/PNGnow2.png"><br>
 281       <br>
 282       Last update 2012-04-16 by <a
 283         href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
 284         Guidi</a><br>
 285     </div>
 286   </body>
 287 </html>