X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fspecification.html;h=41de394776bcc844420082b9933e428e56a0f042;hb=ecb63d645415784352a937f8320f84c23da327f7;hp=ee4fc06a183b7aa9f06ff20f9764bf9d89bb2fcc;hpb=3080bf8226d155d017c5ec5c4e852d952f5b878c;p=helm.git diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html index ee4fc06a1..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,16 +62,20 @@ milestones + + version 2 + + (background - core - applications) + +
+ version 2 - version 2 - - (background - core - applications) - library + (static LDDL directory) @@ -74,31 +84,31 @@ 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, @@ -111,7 +121,7 @@ Delta: after its conclusion, the specification is modified just for maintenance.
-
+
@@ -122,7 +132,23 @@ - + + + + + + + - + + + + + + + + + - + @@ -148,7 +197,10 @@ + + - + +
started announced releasedconcludedconcludedreferences
+ Version 3 + "basic_3" + + + + + + + J3a +
@@ -132,11 +158,34 @@ Matita 0.99.2 "A""A2"October 2015 + + + +
+
+
+ 		+
+ 		+
+ 		"A1" April 2011 June 2014 October 2014 + August 2015 + V2a + R2c +
AbandonedMarch 2008 - February 2011February 2011 +
+
@@ -162,128 +214,149 @@ May 2004 December 2005 November 2006May 2008May 2008 + V1a + J1a +
- - - -
+
+ 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:
- -