+
![[Crux Logo]](download/crux_32.png "The Crux")
@@ -44,25 +43,32 @@
src="download/b5.png">
- 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
+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 permanent λδ URL is sheduled to become http://lambda_delta.info as soon as
-possible.
-
-
- The permanent λδ URL is sheduled to become http://lambda_delta.info on
+December 2012.
+
+
-
-
- April 2011. The
-specification of λδ version 2 is restarted in Matita 0.5.
+specification of λδ version 2 and related topics is restarted in Matita 0.5. +
-
@@ -79,22 +85,15 @@ Permanent λδ URL acquired: http://lambda-de
- September 2009. Helena 0.8.0 is released and the λδ Digital Library is
-started.
+ href="implementation.html#lddl">λδ Digital Library
- June 2009. Helena, A validator for λδ, is
-available
-as
-a
-part
-of
-the HELM software.
+ style="font-style: italic;">Helena, a validator for λδ version 2, is +available as a part of the HELM +software.
- July 2008. First journal paper on λδ accepted + href="documentation.html#ldp5">First journal paper on λδ accepted for publication.
- July 2008. First procedural
-reconstruction in Matita 0.5
-of the λδ proof scripts in
-Coq 7.3.1.
+ href="http://helm.cs.unibo.it/procedural/">procedural reconstruction +for Matita 0.5 of the λδ proof scripts for Coq 7.3.1.
- June 2008. The HTML
-pages of the specification of λδ in Matita 0.5 are online.
+ href="implementation.html#static">HTML pages of the specification of +λδ version 1 for Matita 0.5 are online.
+
+
-
+
- May 2008. The
+specification of λδ version 1 is closed.
- March 2008. The -specification of λδ version 2 in Coq 7.3.1 begins: +specification of λδ version 2 is started with Coq 7.3.1 (false start). +
-
+
- September 2007. The + specification of λδ +version 1 for Matita 0.4 is online.
-
-
- September 2007.
-The specification of λδ in
-Matita 0.4 is online.
-
+ - November 2006. λδ version 1 is released.
- December 2005. First communication on λδ.
+ href="documentation.html#ldt1">First communication on λδ.
- May 2004. The specification of λδ in
-Coq 7.3.1 begins.
+ href="implementation.html#ldp1">specification of λδ version 1 is +started with Coq 7.3.1.
Visibility ![[Butterfly]](download/b4.png "Butterfly")
-
-
- November 2010.
-The Google
-search formal system lambda delta
-gives 8 resources about λδ as the first results.
+ - February 2012. The Google search for formal system lambda delta gives
+5 resources about λδ in the first 6 results.
-
-
- November 2010. -The Yahoo -search formal system lambda delta -gives 4 resources and 2 sub-resources about λδ as the first results. +
- February 2012. The Yahoo search formal system lambda delta gives +this site as the first result.
![[Use Any Browser Here]](download/globe_trans.png "Use Any Browser Here")
![[PNG Used Here]](download/PNGnow2.png "PNG Used Here")
+ title="PNG Used Here" src="download/PNGnow2.png">
-Last update 2011-09-09 by Ferruccio +Last update 2012-11-20 by Ferruccio + Guidi