X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fnews.html;h=498f6487ebd836ffc1f82f0799c0828858199f6d;hb=aeb003ab531d9b9faffd46c47204b564009063cf;hp=7d581cbb7dbaede08fbf3165dc58db6a668d6525;hpb=2a5e0b799cd6aae5d920c67a5ddc9d9888cf7e80;p=helm.git diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index 7d581cbb7..498f6487e 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -1,259 +1,385 @@ - - - - - lambdadelta home page - - - - - -

-[Crux Logo] -

The Formal System λδ (lambdadelta)
-

-

Towards the unification of terms, types, environments and contexts

-[Separator]
- - - - - - - -
+ + + + + + + + + + \lambda\delta home page + + + + + + +
+ + [\lambda\delta home] + +
+
The Formal Systems of the λδ (\lambda\delta) Family
+
+ [Spacer] +
+
+
+
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+ home + + news + + specification + +
+ 		+
+ 		+ documentation + + implementation + +
+
+ foreword + + milestones + + version 2 + (background - core - applications) +
+ 		+ version 2 + + helena + + Open Symbolic Notation (OSN) +
+ citations + + visibility + + version 1 + (background - core)(static HELM directory) + version 1 + + library + (static LDDL directory)
+
+ +
Milestones [butterfly] +
+ + +
    +
  • + 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. +
  • + The translated specification of Landau's "Grundlagen der Analysis" + is validated in CC by Coq 8.4.3. +
    • +
+ + +
    +
  • + 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.
      -
    • News
      • -
    +
  • + The corrected specification of Landau's "Grundlagen der Analysis" + is validated in λδ version 3. +
    • +
+ + + +
    +
  • + July 2014. + A new version of this site is online. +
    • +
+ +
    +
  • + 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": -
-

News [Butterfly]

-
    -
  • September 2011. The -denomination "lambdadelta" changes to "lambdadelta". -
      -
    • 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 permanent λδ URL is sheduled to become http://lambdadelta.info on -December 2012.
      -
      • -
    -
    • -
-
    -
  • April 2011. The -specification of λδ version 2 and related topics is restarted in Matita 0.5. -
      -
    • Here is a page about the -topics related to the specification (Applications).
      • -
    • Here is a page about the -specification (Core).
      • -
    -
    • -
- -
    -
  • November 2010. Helena 0.8.1 is released.
    -
    • -
- - - -
    -
  • September 2008. -This site is online.
    -
    • -
- - - - -
    -
  • May 2008. The -specification of λδ version 1 is closed.
    -
    • -
-
    -
  • March 2008. The -specification of λδ version 2 is started with Coq 7.3.1 (false start).
    • -
- - - - - -

Visibility [Butterfly]

-
    -
  • February 2012. The Google search for formal system lambda delta gives -5 resources about λδ in the first 6 results.
    -
    • -
-
    -
  • February 2012. The Yahoo search formal system lambda delta gives -this site as the first result.
    • -
-
-
-[Valid HTML 4.01 Transitional] [Use Any - Browser Here] [PNG Used Here]
-
-Last update 2012-12-01 by Ferruccio - -Guidi
-
- +
  • + 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. +
    • + + + + + + + + + + + + + + + + + + + + +
    Visibility [butterfly] +
    + + +
    + [Spacer] +
    +
    +
    +
    +
    + + [Valid XHTML 1.1] + + + [Valid CSS level 2] + + + [Generated from XML via XSL] + + + [PNG used here] + + + [Viewable with any browser] + +
    +
    +
    +
    +
    Last update: Wed, 25 Oct 2017 21:44:32 +0200
    +