X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fapps_2%2Fweb%2Fapps_2.ldw.xml;h=dac657eb326a2e9e51d7dd33dd6c0b511194bc36;hb=cfc43911db215e21036317b26bd1dcf9c3e5d435;hp=394568e00b0a750cb78b38e1015d9eb4bf5a17ed;hpb=037b48dbbc0b4373ad1e43d837ac9158787486ef;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml index 394568e00..dac657eb3 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml @@ -8,20 +8,24 @@
Contents of the Specification
This specification comprises a collection of checked applications of λδ version 2. - In particular it contains the components below. + In particular it contains the components below. Martin-Löf's Type Theory with one universe - using λδ as theory of expressions. + using λδ as theory of expressions. The validation algorithm for λδ as implemented in - Helena 0.8. + Helena 0.8. - +
Summary of the Specification
Here is a numerical acount of the specification's contents and its timeline. + Nodes are counted according to the "intrinsinc complexity measure" + [F. Guidi: "Procedural Representation of CIC Proof Terms" + Journal of Automated Reasoning 44(1-2), Springer (February 2010), + pp. 53-78]. @@ -29,7 +33,7 @@ The Functional component is started - inside the specification of λδ version 2. + inside the specification of λδ version 2. The MLTT1 component is started. @@ -39,8 +43,8 @@ The source files are grouped in planes and components according to the following table. Each component contains its own notation file. - The notation for the relations or functions introduced in each file - is shown in parentheses (? are placeholders). + The notation for the relations or functions introduced in each file + is shown in parentheses (? are placeholders).