The Formal System λδ (lambda-delta)

• Foreword

• News

• Papers

• Resources
  

News

• 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. An improvement of the specification of λδ in Coq 7.3.1 begins:
  • native type assignment with new rules for application: nty (it replaces ty3);
    
  • parallel conversion on focalized terms: fpcs (it replaces pc3);
    
  • new weak parallel reduction on environments: wcpr (it is based on fpr and replaces wcpr0); 
    
  • parallel reduction on focalized terms: fpr and fprs (they replace pr2, pr3);
    
  • new thinning relation: drop (it replaces the old drop, clear, getl, cimp, drop1);
  • new shift function: shift: (it replaces app1);
  • new length function for environments: clen;
    
  • new relocation function: lift (it replaces old lift, lift1);
    
  • new term structure with polarity indicators and no distinction between binding and flat items;
  • new general theory of relocation (comprises new relocation functions: s, r);
  • we removed context-free reduction and conversion (pr0, pr1, pc1);
    
  • we removed greedy substitution (csubst0, csubst1, fsubst0, subst0, subst1);
    
  • we removed level indicators on environments (cbk).

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