1 <?xml version="1.0" encoding="UTF-8"?>
3 <page xmlns="http://lambda_delta.info"
4 description = "lambda_delta version 2"
5 title = "lambda_delta version 2"
6 head = "cic:/matita/lambda_delta/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="ld_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
23 <table name="ld_basic_2_sum"/>
24 <news date="In progress.">
25 Context-sensitive strong normalization of simply typed terms.
27 <news date="2012 January 27.">
28 Support for abstract candidates of reducibility closed.
30 <news date="2011 September 21.">
31 Confluence of context-sensitive parallel reduction closed.
33 <news date="2011 September 6.">
34 Confluence of context-free parallel reduction closed.
36 <news date="2011 April 17.">
37 Specification started.
40 <section>Logical Structure of the Specification</section>
41 <body>The source files are grouped in planes and components
42 according to the following table.
43 A notation file covering the whole specification is provided.
44 The notation for the relations or functions introduced in each file
45 is shown in parentheses.
47 <table name="ld_basic_2_src"/>
49 <section>Physical Structure of the Specification</section>
50 <body>The source files are grouped in directories,
51 one for each component.