X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fweb%2Fhome%2Fspecification.ldw.xml;h=2bab97a07446ac1a53cb96bfc51d5d64002cc39c;hb=3080bf8226d155d017c5ec5c4e852d952f5b878c;hp=815f9f34ab17a5928af344296bda1a293ae44cc8;hpb=636db4e12452d2ebce318b36cf5c41d30e4d9c29;p=helm.git diff --git a/helm/www/lambdadelta/web/home/specification.ldw.xml b/helm/www/lambdadelta/web/home/specification.ldw.xml index 815f9f34a..2bab97a07 100644 --- a/helm/www/lambdadelta/web/home/specification.ldw.xml +++ b/helm/www/lambdadelta/web/home/specification.ldw.xml @@ -11,13 +11,26 @@ Î»Î´ is developed as a machine-checked digital specification. It comes in several versions listed in the next table, - which includes the major milestones: + which includes the major milestones. + + + The life cycle of a specification consists of four periods. + + the definitions are designed and the major propositions are proved, + then the calculus is announced with a presentation. + + major changes and additions may occur before the calculus is released on paper. + + subsequent improvements occur until the specification is completed or superseded, + while major changes and additions are announced and reported on paper. + + after its conclusion, the specification is modified just for maintenance. -

Î»Î´ version 2 (in progress)

Î»Î´ version 2 (active)

The formal specification of Î»Î´ version 2 is available in the following formats: @@ -26,11 +39,15 @@ lambdadelta_2 for Matita 0.99.2 - (revised ). + (revised ). Source scripts. - compile with the latest version of Matita from + The scripts are grouped in directories, first by part, then by component. + + + + the scripts are checked by the latest version of Matita from HELM Subversion repository at path <trunk/matita/>. @@ -42,24 +59,42 @@ Core, Applications. + + + nodes are counted according to the "intrinsic complexity measure" + [F. Guidi: "Procedural Representation of CIC Proof Terms" + Journal of Automated Reasoning 44(1-2), Springer (February 2010), pp. 53-78]. + + + + from the logical standpoint, the source scripts are grouped in "planes" + and these are grouped in "components"; + the notation for the relations or functions + introduced in each script, is shown in parentheses (? are placeholders). + -

Î»Î´ version 1 (dismissed)

Î»Î´ version 1 (superseded)

The formal specification of Î»Î´ version 1 is available in the following formats: - lambdadelta_1 for Coq 7.3.1 - (revised ). - Source scripts. + + lambdadelta_1 for Coq 7.3.1 + (revised ). + Source scripts. + + + The scripts are grouped in directories, one for each part. + - lambdadelta_1 for Matita 0.5" - (revised ). + lambdadelta_1 for Matita 0.5 + (revised ). Static HTML pages generated by the HELM rendering engine. @@ -85,10 +120,10 @@ - lambdadelta_1 for Matita 0.5" - (revised ). + lambdadelta_1 for Matita 0.5 + (revised ). HELM directory. - +