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=51995e4fef492cdc4653b4a69f6bc55b24becc31;hpb=335ae5716c5abbdbaaa4f115c56f7fdcc91320a4;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 51995e4fe..86b431c6e 100644 --- a/helm/www/lambda_delta/web/home/basic_2.ldw.xml +++ b/helm/www/lambda_delta/web/home/basic_2.ldw.xml @@ -33,8 +33,11 @@ Extended context-sensitive strong normalization for simply typed terms. + + Confluence for context-free parallel reduction on closures. + - Polarized binders to control ζ reduction. + Term binders polarized to control ζ reduction. Context-sensitive subject equivalence @@ -49,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.