X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fnews.html;h=3971c904e9908f617455ca7b5effcbc00c5c0099;hb=f7d7f2459b3b0409be5f168822be3b836ccc929b;hp=2c1fa2f104d6d50584b2e1d91a9ab7f3d1c09d73;hpb=db4fa4436863ec774b70787659f749542908f227;p=helm.git diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index 2c1fa2f10..3971c904e 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -19,264 +19,342 @@ [lambdadelta home] -
The Formal System λδ (\lambda\delta)
+
The Formal Systems of the λδ (\lambda\delta) Family
[Spacer]
-
+

- - - - - - - + + - - - - - + - - + - - - - + + - - -
- foreword + + home + news - documentation - - implementation + + specification +
+
+ + documentation + + implementation +
-
- 		-
+ 		+ foreword -
+ 		+ milestones - Version 2 + + version 2 - Background + (background - core - applications) +
- Core + + version 2 - Applications + + library (static LDDL directory)
-
+ 		+ citations -
+ 		+ visibility -
+ 		+ version 1 - Version 1 + (background - core)(static HELM directory) + version 1 -
+ 		+ helena -
- 		+
- -
Milestones [spacer] + +
Milestones [spacer]
-
+ + +
    +
  • + August 2015. + The specification of λδ version 2A1 is concluded. +
    • +
+
    +
  • + June 2015. + The corrected specification of Landau's "Grundlagen der Analysis" + is validated in a λProlog implementation of λδ version 3. +
    • +
+
    +
  • + March 2015. + The specification of λδ version 1 is validated by + Matita 0.99.2. +
    • +
+
    +
  • + February 2015. + "Helena 0.8.2" is updated. -
      -
    • - December 2012. - The character "_" is removed from the denomination "lambda_delta": -
        -
      • - The denomination "\lambda\delta" is used in λδ-related texts. -
        • -
      • - The denomination "lambdadelta" is used in λδ-related identifiers. -
        • -
      • - Permanent λδ URL acquired: - http://lambdadelta.info/ - (pointing at this site). -
        • -
      +
    • -
+ +
    +
  • + January 2015. + The specification of λδ version 1 + is updated with backports from the abandoned specification of λδ version 2. +
    • +
+
    +
  • + December 2014. + "Helena 0.8.2" is released.
      -
    • - September 2011. - The denomination "lambda-delta" changes to "lambda_delta": -
        -
      • - The character "-" is reserved in λδ textual syntax - (recognized by "Helena 0.8.1"). -
        • -
      • - Eventually, the occurrences of the character "-" - will be replaced by "_" in all λδ-related identifiers. -
        • -
      • - In particular, this refactoring involves file names and path names. -
        • -
      +
    • + The corrected specification of Landau's "Grundlagen der Analysis" + is validated in λδ version 3.
      • -
    -
    • -
-
    -
  • - December 2010. - Transient λδ URL acquired: http://lambda-delta.info/ (expires on December 2012). +
+ +
    +
  • + July 2014. + A new version of this site is online. +
    • +
+ + +
    +
  • + December 2012. + The character "_" is removed from the denomination "lambda_delta":
      -
    • - November 2010. - "Helena 0.8.1" is released. +
    • + The denomination "\lambda\delta" is used in λδ-related texts.
      • -
    -
      -
    • - September 2009. - "Helena 0.8.0" is released and the - λδ Digital Library - is started. +
    • + The denomination "lambdadelta" is used in λδ-related identifiers.
      • -
    - -
      -
    • - September 2008. - This site is online. +
    • -
+ +
    +
  • + September 2011. + The denomination "lambda-delta" changes to "lambda_delta":
      -
    • - July 2008. - First journal paper on λδ - accepted for publication. +
    • + The character "-" is reserved in λδ textual syntax + (recognized by "Helena 0.8.1").
      • -
    -
      -
    • - July 2008. - First procedural reconstruction - for Matita 0.5 - of the λδ version 1 for Coq 7.3.1. +
    • + Eventually, the occurrences of the character "-" + will be replaced by "_" in all λδ-related identifiers.
      • -
    - -
      -
    • - May 2008. - The specification of λδ version 1 is dismissed. +
    • -
-
    -
  • - March 2008. - The specification of λδ version 2 is started with Coq 7.3.1 (false start). -
    • -
- - - -
    -
  • - May 2004. - The specification of λδ version 1 - is started with Coq 7.3.1. -
    • -
-
- -
Visibility [spacer] + + +
    +
  • + February 2011. + The specification of λδ version 2 with Coq 7.3.1 is abandoned. +
    • +
+
    +
  • + December 2010. + Transient λδ URL acquired: http://lambda-delta.info/ (expires on December 2012). +
    • +
+ + + +
    +
  • + September 2008. + This site is online. +
    • +
+ + + +
    +
  • + May 2008. + The specification of λδ version 1 is concluded. +
    • +
+
    +
  • + March 2008. + The specification of λδ version 2 is started with Coq 7.3.1 (false start). +
    • +
+ + + +
    +
  • + May 2004. + The specification of λδ version 1 + is started with Coq 7.3.1. +
    • +
+ +
Visibility [spacer]
-
-
    -
  • - June 2014. - The Google - search for "formal system lambda delta" gives - 5 resources about λδ in the first 6 results. -
    • -
-
    -
  • - June 2014. - The Yahoo - search for "formal system lambda delta" gives - 4 resources about λδ in the first 5 results. -
    • -
-
- -
+
    +
  • + June 2014. + The Google + search for "formal system lambda delta" gives + 5 resources about the λδ family in the first 6 results. +
    • +
+
    +
  • + June 2014. + The Yahoo + search for "formal system lambda delta" gives + 4 resources about the λδ family in the first 5 results. +
    • +
+
[Spacer]
@@ -302,6 +380,6 @@

-
Last update: Mon, 14 Jul 2014 22:47:32 +0200
- +
Last update: Fri, 01 Apr 2016 23:30:52 +0200
+