The Formal System λδ (lambda_delta)

• Foreword

• News

• Papers

• Resources
  

News

• 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 permanent λδ URL is sheduled to become http://lambda_delta.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).

• December 2010. Permanent λδ URL acquired: http://lambda-delta.info (pointing at this site).
  

• November 2010. Helena 0.8.1 is released.
  

• September 2009. Helena 0.8.0 is released and the λδ Digital Library is started.
  

• June 2009. Helena, a validator for λδ version 2, is available as a part of the HELM software.
  

• September 2008. This site is online.
  

• July 2008. First journal paper on λδ accepted for publication.

• July 2008. First procedural reconstruction for Matita 0.5 of the λδ proof scripts for Coq 7.3.1.
  

• June 2008. The HTML pages of the specification of λδ version 1 for Matita 0.5 are online.
  

• March 2008. The 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.

• November 2006. λδ version 1 is released.

• December 2005. First communication on λδ.
  

• May 2004. The specification of λδ version 1 is started with Coq 7.3.1.
  

Visibility

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