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).