+ $[\lambda\delta home]$

-

+ $\lambda\delta rainbow rule$

+

@@ -31,325 +31,331 @@ - home + home news + + specification + + +
+ + +
+ documentation - specification + implementation - +
- - implementation - - foreword + foreword milestones + + version 2 + + (background - core - applications) + +
+ version 2 - version 2 + helena - (background - core - applications) - - library + + Open Symbolic Notation (OSN) - notice + citations - citations + visibility + + version 1 + + (background - core) + (static HELM directory) version 1 - version 1 - - -
- - - helena + library + (static LDDL directory)

- - - -

Milestones

+ +

Milestones $\lambda\delta butterfly$

- -

- July 2014. - A new version of this site is online. + December 2015. + Second journal paper on Î»Î´ + accepted for publication. +

+ December 2015. + "Helena 0.8.3" is released. +

+ 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. +
- + The corrected specification of Landau's "Grundlagen der Analysis" + is validated in Î»Î´ version 3. +
+

- June 2014. - First communication on Î»Î´ version 2. + October 2014. + Î»Î´ version 2A1 + is released.

- December 2012. + July 2014. + A new version of this site is online. +

+ June 2014. + First communication on Î»Î´ version 2. +

+ 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. + 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.
-

- April 2011. - The specification of Î»Î´ version 2 + April 2011. + The specification of Î»Î´ version 2 and related topics is restarted in Matita 0.5.

- December 2010. + 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).

- November 2010. - "Helena 0.8.1" is released. + November 2010. + "Helena 0.8.1" is released.

- September 2009. - "Helena 0.8.0" is released and the - Î»Î´ Digital Library - is started. + September 2009. + "Helena 0.8.0" is released and the + Î»Î´ Digital Library is started.

- June 2009. + June 2009. "Helena", a validator for Î»Î´ version 2, is available as a part of the HELM software.

- September 2008. + September 2008. This site is online.

- July 2008. - First journal paper on Î»Î´ + July 2008. + First journal paper on Î»Î´ accepted for publication.

- July 2008. + July 2008. First procedural reconstruction for Matita 0.5 of the Î»Î´ version 1 for Coq 7.3.1.

- June 2008. - The + June 2008. + The HTML pages of the specification of Î»Î´ version 1 for Matita 0.5 are online.

- May 2008. - The specification of Î»Î´ version 1 is dismissed. + May 2008. + The specification of Î»Î´ version 1 is concluded.

- March 2008. + March 2008. The specification of Î»Î´ version 2 is started with Coq 7.3.1 (false start).

- September 2007. - The + September 2007. + The specification of Î»Î´ version 1 for Matita 0.4 is online.

- November 2006. - Î»Î´ version 1 + November 2006. + Î»Î´ version 1 is released.

- December 2005. - First communication on Î»Î´ version 1. + December 2005. + First communication on Î»Î´ version 1.

- May 2004. - The specification of Î»Î´ version 1 + May 2004. + The specification of Î»Î´ version 1 is started with Coq 7.3.1.

Citations

-

- Here is a list of publications citing Î»Î´ (not including our own). -

- A. Asperti, W. Ricciotti, C. Sacerdoti Coen, E. Tassi: - Formal metatheory of programming languages in the Matita interactive theorem prover - (2012). In JAR 49(3), pp. 427-451. -

- M.E. Maietti: - Consistency of the minimalist foundation with Church thesis and Bar Induction - (2012). Submitted article. -

- W. Ricciotti: - Theoretical and implementation aspects in the mechanization of the metatheory of programming languages - (July 2011). Ph.D. Thesis in Computer Science, Technical Report UBLCS-2011-09, University of Bologna. -

- C.E. Brown: - Faithful Reproductions of the Automath Landau Formalization - (2011). Typescript note. -

- M.E. Maietti: - A minimalist two-level foundation for constructive mathematics - (2009). In APAL 160(3), pp. 319-354. -

- V. Rahili: - First Year Report: Realisability methods of proof and semantics with application to expansion - (July 2007). Typescript note. -

Visibility [spacer]

+ +

Visibility $\lambda\delta butterfly$

- -

- June 2014. + June 2014. 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.

- June 2014. + June 2014. 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.

-

+

+ $\lambda\delta rainbow rule$

@@ -374,6 +380,6 @@

-

Last update: Mon, 20 Oct 2014 16:37:19 +0200

- +

Last update: Fri, 22 Jul 2016 19:34:08 +0200

+