|
News ![Butterfly [Butterfly]](download/b5.png)
- November 2010. Helena 0.8.1 is released.
- September 2008.
This site is 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).
Visibility ![Butterfly [Butterfly]](download/b4.png)
- 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.
|