1 <?xml version="1.0" encoding="UTF-8"?>
3 <page xmlns="http://lambdadelta.info/"
4 description = "\lambda\delta version 2"
5 title = "\lambda\delta version 2"
6 head = "cic:/matita/lambdadelta/basic_2/ (λδ version 2)"
9 <section>System's Syntax and Behavior</section>
10 <body>This is a summary of the "block structure"
11 of the System's syntactic items and reductions.
13 <table name="basic_2_blk"/>
14 <body>* In terms only.
15 ** In terms and local environments only.
16 *** In global environments only.
17 **** Sort level k in terms only.
21 <section>Summary of the Specification</section>
22 <body>Here is a numerical acount of the specification's contents
25 <table name="basic_2_sum"/>
27 <subsection>Stage "B"</subsection>
28 <news class="alpha" date="Ongoing.">
29 Context-sensitive subject equivalence
30 for native type assignment.
33 <subsection>Stage "A": "Weakening the Applicability Condition"</subsection>
34 <news class="beta" date="2014 September 9.">
35 Iterated static type assignment defined (more elegantly)
36 as a primitive notion.
38 <news class="beta" date="2014 June 18.">
39 Preservation of stratified native validity
40 for context-sensitive computation on terms.
42 <news class="alpha" date="2014 June 9.">
43 Strong qrst-normalization
44 for simply typed terms.
46 <news class="alpha" date="2014 April 16.">
47 Lazy equivalence on local environments
48 addded as q-step to rst-computation on closures
49 (anniversary milestone).
51 <news class="alpha" date="2014 January 20.">
52 Parametrized slicing of local environments
53 comprises both versions of this operation
54 (one from basic_1, the other used in basic_2 till now).
56 <news class="alpha" date="2013 August 7.">
57 Passive support for global environments.
59 <news class="alpha" date="2013 July 27.">
60 Reaxiomatized β-reductum as in rt-reduction.
62 <news class="alpha" date="2013 July 20.">
63 Context-sensitive strong rt-normalization
64 for simply typed terms.
66 <news class="alpha" date="2013 April 16.">
67 Reaxiomatized substitution and reduction
68 commute with respect to subclosure
69 (anniversary milestone).
71 <news class="alpha" date="2013 March 16.">
72 Mutual recursive preservation of stratified native validity
73 for rst-computation on closures.
75 <news class="alpha" date="2012 October 16.">
76 Confluence for context-free parallel reduction on closures.
78 <news class="alpha" date="2012 July 26.">
79 Term binders polarized to control ζ-reduction (not released).
81 <news class="alpha" date="2012 April 16.">
82 Context-sensitive subject equivalence
83 for atomic arity assignment
84 (anniversary milestone).
86 <news class="alpha" date="2012 March 15.">
87 Context-sensitive strong normalization
88 for simply typed terms.
90 <news class="alpha" date="2012 January 27.">
91 Support for abstract candidates of reducibility.
93 <news class="alpha" date="2011 September 21.">
94 Confluence for context-sensitive parallel reduction on terms.
96 <news class="alpha" date="2011 September 6.">
97 Confluence for context-free parallel reduction on terms.
99 <news class="alpha" date="2011 April 17.">
100 Specification starts.
103 <section>Logical Structure of the Specification</section>
104 <body>The source files are grouped in planes and components
105 according to the following table.
106 Notation files covering the whole specification are provided.
107 The notation for the relations or functions introduced in each file
108 is shown in parentheses (? are placeholders).
110 <table name="basic_2_src"/>