X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Flambdadelta%2Fspecification.html;h=41de394776bcc844420082b9933e428e56a0f042;hb=f7d7f2459b3b0409be5f168822be3b836ccc929b;hp=74d092b40cf6aa0bd6ac75f64e21d4d55415f435;hpb=1f1eb9d91faf1e905d44b5f44943b2db8472cc74;p=helm.git diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html index 74d092b40..41de39477 100644 --- a/helm/www/lambdadelta/specification.html +++ b/helm/www/lambdadelta/specification.html @@ -19,11 +19,11 @@ [lambdadelta home] -
The Formal System λδ (\lambda\delta)
+
The Formal Systems of the λδ (\lambda\delta) Family
[Spacer]
-
+

@@ -36,18 +36,24 @@ news + + specification + + +
+ + +
+ documentation - specification + implementation - +
- - implementation - @@ -56,49 +62,66 @@ milestones + + version 2 + + (background - core - applications) + +
+ version 2 - version 2 - - (background - core - applications) - library + (static LDDL directory) - notice + 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: +
+ The systems of the λδ family are developed as machine-checked digital specifications, + and are listed in the next table, 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 +132,23 @@ - + + + + + + + - + + + + + + + + + - - + + + + + + + + + + - + +
started announced releaseddismissedconcludedreferences
+ Version 3 + "basic_3" + + + + + + + J3a +
@@ -119,11 +158,49 @@ Matita 0.99.2 "A""A2"October 2015 + + + +
+
+
+ 		+
+ 		+
+ 		"A1" April 2011 June 2014Planned in October 2014Not planned yetOctober 2014August 2015 + V2a + R2c +
Abandoned + + Coq 7.3.1 + + March 2008 + + February 2011 +
+
@@ -137,99 +214,149 @@ May 2004 December 2005 November 2006May 2008May 2008 + V1a + J1a +
- - - -
- [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 3 (proposed)
+
+ The formal specification of λδ version 3 + is forthcoming. +
+ +
+ [spacer] λδ version 2 (active)
+
The formal specification of λδ version 2 is available in the following formats:
- -