X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Flambdadelta%2Fspecification.html;h=2abf3281e503b4fbc8590c8bcbf7caa5a93115a3;hb=32def68dd99ad5f20f001e3e76b51afa6f69dec5;hp=4ecf9994cc69fcc390c16feb17b850388058ef31;hpb=636db4e12452d2ebce318b36cf5c41d30e4d9c29;p=helm.git diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html index 4ecf9994c..2abf3281e 100644 --- a/helm/www/lambdadelta/specification.html +++ b/helm/www/lambdadelta/specification.html @@ -23,7 +23,7 @@
[Spacer]
-
+

@@ -36,18 +36,24 @@ news + + specification + + +
+ + +
+ documentation - specification + implementation - +
- - implementation - @@ -56,49 +62,67 @@ milestones + + version 2 + + (background - core - applications) + +
+ version 2 - version 2 - - (background - core - applications) - library + (static LDDL directory) - notice + citations - citations + visibility + + + version 1 + (background - core) + (static HELM directory) version 1 - version 1 + helena - +
- - helena -
- -
Computer-checked formal specifications [spacer] +
Computer-checked formal specifications [spacer]
-
+
λδ 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. + Alpha: + the definitions are designed and the major propositions are proved, + then the calculus is announced with a presentation. + Beta: + major changes and additions may occur before the calculus is released on paper. + Gamma: + subsequent improvements occur until the specification is completed or superseded, + while major changes and additions are announced and reported on paper. + Delta: + after its conclusion, the specification is modified just for maintenance.
-
+
@@ -109,7 +133,7 @@ - + - - + + + + + + +
started announced releaseddismissedconcluded
@@ -122,8 +146,20 @@ "A" April 2011 June 2014Planned in October 2014In progressOctober 2014 +
Abandoned + + Coq 7.3.1 + + March 2008 + + February 2011
@@ -142,101 +178,131 @@
- - - -
- [spacer] λδ version 2 (in progress)
-
+
+ Informational pages on the specifications are provided. +
+
    +
  • + Notice on displayed numerical acounts: + 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]. +
    • +
+
    +
  • + Notice on displayed logical structures: + 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). +
    • +
+ +
+ [spacer] λδ version 2 (active)
+
The formal specification of λδ version 2 is available in the following formats:
- -