X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambda_delta%2Fweb%2Fhome%2Fbasic_2.ldw.xml;h=86b431c6e8e2a956a996261c8c5b255bac723448;hb=0fa1d4541bec571d84c726c488ba500a269bfb07;hp=6a1f302397723da71e55f3ce78a8574f545b3203;hpb=ae7427e8d3c57ccc77931e27913d8605d385cbda;p=helm.git
diff --git a/helm/www/lambda_delta/web/home/basic_2.ldw.xml b/helm/www/lambda_delta/web/home/basic_2.ldw.xml
index 6a1f30239..86b431c6e 100644
--- a/helm/www/lambda_delta/web/home/basic_2.ldw.xml
+++ b/helm/www/lambda_delta/web/home/basic_2.ldw.xml
@@ -26,8 +26,23 @@
for native type assignment.
+ Closure of extended context-sensitive computation
+ for native validity.
+
+
+ Extended context-sensitive strong normalization
+ for simply typed terms.
+
+
+ Confluence for context-free parallel reduction on closures.
+
+
+ Term binders polarized to control ζ reduction.
+
+
Context-sensitive subject equivalence
- for atomic arity assignment.
+ for atomic arity assignment
+ (anniversary milestone).
Context-sensitive strong normalization
@@ -37,10 +52,10 @@
Support for abstract candidates of reducibility.
- Confluence for context-sensitive parallel reduction.
+ Confluence for context-sensitive parallel reduction on terms.
- Confluence for context-free parallel reduction.
+ Confluence for context-free parallel reduction on terms.
Specification starts.
@@ -51,7 +66,7 @@
according to the following table.
A notation file covering the whole specification is provided.
The notation for the relations or functions introduced in each file
- is shown in parentheses.
+ is shown in parentheses (? are placeholders).