1 <?xml version="1.0" encoding="UTF-8"?>
3 <page xmlns="http://lambdadelta.info/"
4 description = "\lambda\delta home page"
5 title = "\lambda\delta home page"
7 head = "cic:/matita/lambdadelta/basic_2A/ (core λδ version 2A)"
9 <sitemap name="sitemap"/>
11 <section4 name="summary">Summary of the Specification</section4>
12 <body>Here is a numerical account of the specification's contents
15 <table name="basic_2A_sum"/>
17 <news class="delta" date="2020-02-27.">
18 λδ-2A is repackaged without λδ-ground.
20 <news class="delta" date="2019-11-20.">
21 λδ-2A is repackaged (was λδ-2A1).
23 <news class="delta" date="2015-08-27.">
24 λδ-2A appears too complex and is dismissed.
26 <news class="gamma" date="2014-10-28.">
29 <news class="beta" date="2014-09-09.">
30 Iterated static type assignment defined (more elegantly)
31 as a primitive notion.
33 <news class="beta" date="2014-06-18.">
34 Preservation of stratified native validity
35 for context-sensitive computation on terms.
37 <news class="alpha" date="2014-06-09.">
38 Strong qrst-normalization
39 for simply typed terms.
41 <news class="alpha" date="2014-04-16.">
42 Lazy equivalence on local environments
43 added as q-step to rst-computation on closures
44 (anniversary milestone).
46 <news class="alpha" date="2014-01-20.">
47 Parametrized slicing on local environments
48 comprises both versions of this operation
49 (one from basic_1, the other used in basic_2 till now).
51 <news class="alpha" date="2013-08-07.">
52 Passive support for global environments.
54 <news class="alpha" date="2013-07-27.">
55 Reaxiomatized β-reductum as in rt-reduction.
57 <news class="alpha" date="2013-07-20.">
58 Context-sensitive strong rt-normalization
59 for simply typed terms.
61 <news class="alpha" date="2013-04-16.">
62 Reaxiomatized substitution and reduction
63 commute with respect to subclosure
64 (anniversary milestone).
66 <news class="alpha" date="2013-03-16.">
67 Mutual recursive preservation of stratified native validity
68 for rst-computation on closures.
70 <news class="alpha" date="2012-10-16.">
71 Confluence for context-free parallel reduction on closures.
73 <news class="alpha" date="2012-07-26.">
74 Term binders polarized to control ζ-reduction (not released).
76 <news class="alpha" date="2012-04-16.">
77 Context-sensitive subject equivalence
78 for atomic arity assignment
79 (anniversary milestone).
81 <news class="alpha" date="2012-03-15.">
82 Context-sensitive strong normalization
83 for simply typed terms.
85 <news class="alpha" date="2012-01-27.">
86 Generic candidates of reducibility.
88 <news class="alpha" date="2011-09-21.">
89 Confluence for context-sensitive parallel reduction on terms.
91 <news class="alpha" date="2011-09-06.">
92 Confluence for context-free parallel reduction on terms.
94 <news class="alpha" date="2011-04-17.">
98 <section4 name="structure">Logical Structure of the Specification</section4>
99 <body>This table reports the specification's components and their planes.
101 <table name="basic_2A_src"/>