X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fweb%2Fhome%2Fnews.ldw.xml;h=0bf2256247aadd65f0e1a195c3f4ef6371ca36e0;hb=503426723b9fc786c69dc988d38726997ecb809a;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..0bf225624 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, 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.