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 as soon as possible.
  

• April 2011. The specification of λδ version 2 is restarted in Matita 0.5.
  

• 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 λδ, 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 in Matita 0.5 of the λδ proof scripts in Coq 7.3.1.
  

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

• March 2008. The specification of λδ version 2 in Coq 7.3.1 begins:

• September 2007. The specification of λδ in Matita 0.4 is online.
  

• December 2005. First communication on λδ.
  

• May 2004. The specification of λδ in Coq 7.3.1 begins.
  

Visibility

• November 2010. The Google search formal system lambda delta gives 8 resources about λδ as the first results.
  

• November 2010. The Yahoo search formal system lambda delta gives 4 resources and 2 sub-resources about λδ as the first results.