cic:/matita/lambdadelta/basic_2A/ (core λδ version 2A)

Summary of the Specification

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