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

@@ -45,9 +45,15 @@
- + +
+ + implementation + +
+ @@ -63,16 +69,20 @@ version 2 (background - core - applications) - + +
+ + library + (static LDDL directory) - notice + citations - citations + visibility version 1 @@ -80,25 +90,39 @@ version 1 - -
- - + (background - core) + (static HELM directory) + 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:
- -