X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fnews.html;h=fdf90985729cad32152f059d9f4db1a9c43cff9b;hb=d64caa33426da23e1ab75eca50f227c40e95a24b;hp=f526a75a9b98c2190a52a0000630ef62327f24b1;hpb=7f349a4f0175068138a341081d0dd14fd9fe4c4a;p=helm.git diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index f526a75a9..fdf909857 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -16,252 +16,346 @@
- [lambdadelta home] + [\lambda\delta home]
-
The Formal System λδ (\lambda\delta)
+
The Formal Systems of the λδ (\lambda\delta) Family
- [Spacer] + [Spacer]
-
+

- - - + + + - - - + - + + - - - - - - - + + - +
- home + + home + news + + specification + +
+ 		+
+ 		documentation + implementation +
- Foreword + + foreword + + milestones - Milestones + + version 2 + (background - core - applications) +
- Version 2 + + version 2 - Version 2 + + helena - Background - Core - Applications + + Open Symbolic Notation (OSN)
- Notice + + citations - Visibility + + visibility - Version 1 + + version 1 - Version 1 + (background - core)(static HELM directory) + version 1 -
+ 		+ library (static LDDL directory)
- -
Milestones [spacer] + +
Milestones [butterfly]
-
- -
    -
  • - 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). -
      • -
    -
    • -
-
    -
  • - 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. -
      • -
    -
    • -
- + + +
    +
  • + 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 2010. - Transient λδ URL acquired: http://lambda-delta.info/ (expires on December 2012). +
    • + The translated specification of Landau's "Grundlagen der Analysis" + is validated in CC by Coq 8.4.3.
      • -
    -
      -
    • - November 2010. - "Helena 0.8.1" is released. +
    • -
+ +
    +
  • + 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 2009. - "Helena 0.8.0" is released and the - λδ Digital Library - is started. +
    • + The corrected specification of Landau's "Grundlagen der Analysis" + is validated in λδ version 3.
      • -
    -
    • -
-
    -
  • - September 2008. - This site is online. +
+ +
    +
  • + July 2014. + A new version of this site is online. +
    • +
+ + + + +
    +
  • + September 2011. + The denomination "lambda-delta" changes to "lambda_delta":
      -
    • - March 2008. - The specification of λδ version 2 is started with Coq 7.3.1 (false start). +
    • + The character "-" is reserved in λδ textual syntax + (recognized by "Helena 0.8.1").
      • -
    - -
      -
    • - November 2006. - λδ version 1 - is released. +
    • + In particular, this refactoring involves file names and path names.
      • -
    - -
    • -
-
- -
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 [butterfly]
-
-
    -
  • - 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. -
    • -
-
- -
- [Spacer] +
    +
  • + 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]

@@ -286,6 +380,6 @@

-
Last update: Sun, 20 Jul 2014 11:29:55 +0200
- +
Last update: Tue, 24 Jan 2017 18:22:20 +0100
+