X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fspecification.html;h=4095590fbd5e925557b57089ce2885a679ffba9f;hb=348f1670b30f52db99187b2e92b45348e18ebbbe;hp=cc43bdc0f774d63c6d75b8ac3af19d1b4ad41626;hpb=fe00a22101acb7995f8488a4434c4046bc540af0;p=helm.git
diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html
index cc43bdc0f..4095590fb 100644
--- a/helm/www/lambdadelta/specification.html
+++ b/helm/www/lambdadelta/specification.html
@@ -16,12 +16,12 @@
Computer-checked formal specifications
![lambdadelta butterfly [spacer]](http://lambdadelta.info/images/b5.png)
+
Computer-checked formal specifications
- λδ 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.
@@ -121,59 +127,128 @@
version |
name |
- developed with |
stage |
+ developed with |
started |
announced |
released |
- concluded |
+ concluded |
+ references |
+
+
+
+ Version 3
+ |
+ "basic_3" |
+ |
+ |
+ |
+ |
+ |
+ |
+
+ J3a
+ |
Version 2
|
"basic_2" |
+ "A2" |
+
+ Matita 0.99.3
+ |
+ October 2015 |
+ |
+ |
+ |
+ |
+
+
+
+
+ |
+
+
+ |
+ "A1" |
Matita 0.99.2
|
- "A" |
April 2011 |
June 2014 |
October 2014 |
- |
+ August 2015 |
+
+ V2a
+ R2c
+ |
Abandoned |
|
+ |
Coq 7.3.1
|
- |
March 2008 |
|
|
- February 2011 |
+ February 2011 |
+ |
Version 1
|
"basic_1" |
+ |
Coq 7.3.1
|
- |
May 2004 |
December 2005 |
November 2006 |
- May 2008 |
+ May 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).
+
+
+
+
+
![\lambda\delta butterfly [spacer]](http://lambdadelta.info/images/b8.png)
λδ version 3 (proposed)
+
+ The formal specification of λδ version 3
+ is forthcoming.
+
-
![lambdadelta butterfly [spacer]](http://lambdadelta.info/images/b4.png)
λδ version 2 (active)
+
![\lambda\delta butterfly [spacer]](http://lambdadelta.info/images/b4.png)
λδ version 2 (active)
The formal specification of λδ version 2
is available in the following formats:
@@ -181,9 +256,10 @@
-
The scripts are grouped in directories, first by part, then by component.
@@ -201,23 +277,10 @@
Background,
Core,
Applications.
-
-
- Notice on 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).
-
![lambdadelta butterfly [spacer]](http://lambdadelta.info/images/b6.png)
λδ version 1 (superseded)
+
λδ version 1 (superseded)
The formal specification of λδ version 1
is available in the following formats:
@@ -226,8 +289,9 @@
lambdadelta_1 for Coq 7.3.1
- (revised
2015-01).
+ (revised
2015-09).
Source scripts.
+
Documentation (J1a).
-
2015 January 15.
@@ -283,8 +347,13 @@
Notice: the HELM rendering engine is offline.
+
+ Informational pages on the parts of the specification:
+
Background,
+
Core.
+
-
![lambdadelta rainbow rule [Spacer]](http://lambdadelta.info/images/rainbow.png)
+
@@ -309,6 +378,6 @@
-
Last update: Thu, 15 Jan 2015 16:59:16 +0100
+
Last update: Sun, 22 May 2016 15:25:26 +0200