X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Flambdadelta%2Fspecification.html;h=41de394776bcc844420082b9933e428e56a0f042;hb=ecb63d645415784352a937f8320f84c23da327f7;hp=4bc159e6ddce3e8c7342a420f291718711bd6977;hpb=f72807cb8834aa8991919e365b57d553e3674908;p=helm.git
diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html
index 4bc159e6d..41de39477 100644
--- a/helm/www/lambdadelta/specification.html
+++ b/helm/www/lambdadelta/specification.html
@@ -19,7 +19,7 @@
-
- λδ 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.
@@ -136,6 +135,21 @@
concluded |
references |
+
+
+ Version 3
+ |
+ "basic_3" |
+ |
+ |
+ |
+ |
+ |
+ |
+
+ J3a
+ |
+
Version 2
@@ -212,7 +226,7 @@
Informational pages on the specifications are provided.
-
+
-
Notice on displayed numerical acounts:
nodes are counted according to the "intrinsic complexity measure"
@@ -220,7 +234,7 @@
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"
@@ -229,6 +243,13 @@
introduced in each script, is shown in parentheses (? are placeholders).
+
+
+ λδ version 3 (proposed)
+
+ The formal specification of λδ version 3
+ is forthcoming.
+
λδ version 2 (active)
@@ -361,6 +382,6 @@
- Last update: Thu, 10 Dec 2015 16:21:42 +0100
+ Last update: Fri, 01 Apr 2016 23:30:52 +0200
|