X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fweb%2Fhome%2Fnews.ldw.xml;h=3f1c9f893e136452c8b5a1d3bbf6d47e80cb62e8;hb=0af3592e3a85a4bb82c5c6df259cf9ab117ba0b1;hp=92dda54917a39bee3188888dec8f5bf905525666;hpb=bda6d964ce9729a694e3fd3ead386ca9f2ca14e3;p=helm.git diff --git a/helm/www/lambdadelta/web/home/news.ldw.xml b/helm/www/lambdadelta/web/home/news.ldw.xml index 92dda5491..3f1c9f893 100644 --- a/helm/www/lambdadelta/web/home/news.ldw.xml +++ b/helm/www/lambdadelta/web/home/news.ldw.xml @@ -3,21 +3,73 @@ - Milestones + - + Milestones + + + Second journal paper on λδ + accepted for publication. + + + + "Helena 0.8.3" is released. + + + + The specification of λδ version 2A1 is concluded. + + + + The corrected specification of Landau's "Grundlagen der Analysis" + is validated in a λProlog implementation of λδ version 3. + + + + The specification of λδ version 1 is validated by + Matita 0.99.2. + + + + "Helena 0.8.2" is updated. + + The translated specification of Landau's "Grundlagen der Analysis" + is validated in CC by Coq 8.4.3. + + + + + The specification of λδ version 1 + is updated with backports from the abandoned specification of λδ version 2. + + + + "Helena 0.8.2" is released. + + The corrected specification of Landau's "Grundlagen der Analysis" + is validated in λδ version 3. + + + + + λδ version 2A1 + is released. + + + A new version of this site is online. - - First communication on λδ version 2. + + First communication on λδ version 2. - + The character "_" is removed from the denomination "lambda_delta": The denomination "\lambda\delta" is used in λδ-related texts. @@ -30,7 +82,7 @@ - + The denomination "lambda-delta" changes to "lambda_delta": The character "-" is reserved in λδ textual syntax @@ -43,92 +95,97 @@ - - The specification of λδ version 2 + + The specification of λδ version 2 and related topics is restarted in Matita 0.5. - + + The specification of λδ version 2 with Coq 7.3.1 is abandoned. + + + Transient λδ URL acquired: http://lambda-delta.info/ (expires on December 2012). - - "Helena 0.8.1" is released. + + "Helena 0.8.1" is released. - - "Helena 0.8.0" is released and the - λδ Digital Library - is started. + + "Helena 0.8.0" is released and the + λδ Digital Library is started. - - "Helena", a validator for λδ version 2, + + "Helena", a validator for λδ version 2, is available as a part of the HELM software. - + This site is online. - - First journal paper on λδ + + First journal paper on λδ accepted for publication. - + First procedural reconstruction for Matita 0.5 of the λδ version 1 for Coq 7.3.1. - - The + + The HTML pages of the specification of λδ version 1 for Matita 0.5 are online. - - The specification of λδ version 1 is dismissed. + + The specification of λδ version 1 is concluded. - + The specification of λδ version 2 is started with Coq 7.3.1 (false start). - - The + + The specification of λδ version 1 for Matita 0.4 is online. - - λδ version 1 + + λδ version 1 is released. - - First communication on λδ version 1. + + First communication on λδ version 1. - - The specification of λδ version 1 + + The specification of λδ version 1 is started with Coq 7.3.1. - Visibility + + + Visibility - + The Google search for "formal system lambda delta" gives - 5 resources about λδ in the first 6 results. + 5 resources about the λδ family in the first 6 results. - + The Yahoo search for "formal system lambda delta" gives - 4 resources about λδ in the first 5 results. + 4 resources about the λδ family in the first 5 results.