cic:/matita/lambdadelta/basic_2A/ (core λδ version 2A)
Summary of the Specification
![[butterfly]](http://helm.cs.unibo.it/lambdadelta/images/b4.png "\lambda\delta butterfly")
Here is a numerical account of the specification's contents
and its timeline.
| category | units |
|
|
|
|
|
| sizes | characters (files) | 393236 (343) | nodes (objects) | 1710019 (1605) | intrinsic loss factor | 4.3 |
| propositions | theorems | 119 | lemmas | 1185 | total | 1304 |
| concepts | declared | 50 | defined | 87 | total | 137 |
- 2020-02-27.
λδ-2A is repackaged without λδ-ground.
- 2019-11-20.
λδ-2A is repackaged (was λδ-2A1).
- 2015-08-27.
λδ-2A appears too complex and is dismissed.
- 2014-10-28.
λδ-2A is released.
- 2014-09-09.
Iterated static type assignment defined (more elegantly)
as a primitive notion.
- 2014-06-18.
Preservation of stratified native validity
for context-sensitive computation on terms.
- 2014-06-09.
Strong qrst-normalization
for simply typed terms.
- 2014-04-16.
Lazy equivalence on local environments
added as q-step to rst-computation on closures
(anniversary milestone).
- 2014-01-20.
Parametrized slicing on local environments
comprises both versions of this operation
(one from basic_1, the other used in basic_2 till now).
- 2013-08-07.
Passive support for global environments.
- 2013-07-27.
Reaxiomatized β-reductum as in rt-reduction.
- 2013-07-20.
Context-sensitive strong rt-normalization
for simply typed terms.
- 2013-04-16.
Reaxiomatized substitution and reduction
commute with respect to subclosure
(anniversary milestone).
- 2013-03-16.
Mutual recursive preservation of stratified native validity
for rst-computation on closures.
- 2012-10-16.
Confluence for context-free parallel reduction on closures.
- 2012-07-26.
Term binders polarized to control ζ-reduction (not released).
- 2012-04-16.
Context-sensitive subject equivalence
for atomic arity assignment
(anniversary milestone).
- 2012-03-15.
Context-sensitive strong normalization
for simply typed terms.
- 2012-01-27.
Generic candidates of reducibility.
- 2011-09-21.
Confluence for context-sensitive parallel reduction on terms.
- 2011-09-06.
Confluence for context-free parallel reduction on terms.
- 2011-04-17.
λδ-2A is started.
Last update: Tue, 22 Dec 2020 18:19:03 +0100
![[\lambda\delta home]](http://helm.cs.unibo.it/lambdadelta/images/crux_32.png "\lambda\delta home")
![[Spacer]](http://helm.cs.unibo.it/lambdadelta/images/rainbow.png "\lambda\delta rainbow rule")
![[Generated from XML via XSL]](http://helm.cs.unibo.it/lambdadelta/images/xml_xsl2.png "Generated from XML via XSL")
![[PNG used here]](http://helm.cs.unibo.it/lambdadelta/images/PNGnow2.png "PNG used here")
![[Viewable with any browser]](http://www.anybrowser.org/campaign/bvgraphics/abtfile.png "Viewable with any browser")