1 <?xml version="1.0" encoding="UTF-8"?>
3 <page xmlns="http://lambdadelta.info/"
4 description = "lambdadelta version 2"
5 title = "lambdadelta version 2"
6 head = "cic:/matita/lambdadelta/basic_2/ (λδ version 2)"
8 <section>System's Syntax and Behavior</section>
9 <body>This is a summary of the "block structure"
10 of the System's syntactic items and reductions.
12 <table name="basic_2_blk"/>
13 <body>* In terms only.
14 ** In terms and local environments only.
15 *** In global environments only.
16 **** Sort level k in terms only.
19 <section>Summary of the Specification</section>
20 <body>Here is a numerical acount of the specification's contents
22 Nodes are counted according to the "intrinsinc complexity measure"
23 [F. Guidi: "Procedural Representation of CIC Proof Terms"
24 Journal of Automated Reasoning 44(1-2), Springer (February 2010),
27 <table name="basic_2_sum"/>
28 <news date="In progress.">
29 Context-sensitive subject equivalence
30 for native type assignment.
32 <news date="In progress.">
33 Closure of context-sensitive extended computation
36 <news date="2013 August 7.">
37 Passive support for global environments.
39 <news date="2013 July 27.">
40 Reaxiomatized β-reductum as in extended β-reduction
42 <news date="2013 July 20.">
43 Context-sensitive extended strong normalization
44 for simply typed terms.
46 <news date="2013 April 16.">
47 Reaxiomatized substitution and reduction
48 commute with respect to subclosure
49 (anniversary milestone).
51 <news date="2013 March 16.">
52 Mutual recursive preservation of stratified native validity
53 for "big tree" computation on closures.
55 <news date="2012 October 16.">
56 Confluence for context-free parallel reduction on closures.
58 <news date="2012 July 26.">
59 Term binders polarized to control ζ-reduction.
61 <news date="2012 April 16.">
62 Context-sensitive subject equivalence
63 for atomic arity assignment
64 (anniversary milestone).
66 <news date="2012 March 15.">
67 Context-sensitive strong normalization
68 for simply typed terms.
70 <news date="2012 January 27.">
71 Support for abstract candidates of reducibility.
73 <news date="2011 September 21.">
74 Confluence for context-sensitive parallel reduction on terms.
76 <news date="2011 September 6.">
77 Confluence for context-free parallel reduction on terms.
79 <news date="2011 April 17.">
83 <section>Logical Structure of the Specification</section>
84 <body>The source files are grouped in planes and components
85 according to the following table.
86 A notation file covering the whole specification is provided.
87 The notation for the relations or functions introduced in each file
88 is shown in parentheses (? are placeholders).
90 <table name="basic_2_src"/>
92 <section>Physical Structure of the Specification</section>
93 <body>The source files are grouped in directories,
94 one for each component.