X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambda_delta%2Fweb%2Fhome%2Fld_basic_2.ldw.xml;h=a542cc19a1838dc5a9cab45f2f6dc565c9821312;hb=afe1661e69d1fdec2a65abe1ea9abdae03874967;hp=7a1eef5f79965ae128ce8765702614aa0a2c4821;hpb=ff11fcced84c3e18f0f73be101bc7b2086fc0a52;p=helm.git diff --git a/helm/www/lambda_delta/web/home/ld_basic_2.ldw.xml b/helm/www/lambda_delta/web/home/ld_basic_2.ldw.xml index 7a1eef5f7..a542cc19a 100644 --- a/helm/www/lambda_delta/web/home/ld_basic_2.ldw.xml +++ b/helm/www/lambda_delta/web/home/ld_basic_2.ldw.xml @@ -3,7 +3,7 @@

System's Syntax and Behavior

This is a summary of the "block structure" @@ -20,21 +20,30 @@ Here is a numerical acount of the specification's contents and its timeline. - +

- Context-sensitive strong normalization of simply typed terms. + Context-sensitive subject equivalence + for native type assignment. + + + Context-sensitive subject equivalence + for atomic arity assignment. + + + Context-sensitive strong normalization + for simply typed terms. - Support for abstract candidates of reducibility closed. + Support for abstract candidates of reducibility. - Confluence of context-sensitive parallel reduction closed. + Confluence for context-sensitive parallel reduction. - Confluence of context-free parallel reduction closed. + Confluence for context-free parallel reduction. - Specification started. + Specification starts.

Logical Structure of the Specification