X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Flambdadelta%2Fspecification.html;h=b86e965c0073796c78a4fb8548503f933ab670d8;hb=8653dd54c57943e28e3ef60d2d0cbc1861a76a33;hp=043b472e1fdda1b553768912356c30d3bb34604e;hpb=b01cc7ea6a6a931e3485fde7ec78b2c216918e11;p=helm.git
diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html
index 043b472e1..b86e965c0 100644
--- a/helm/www/lambdadelta/specification.html
+++ b/helm/www/lambdadelta/specification.html
@@ -16,12 +16,12 @@
Computer-checked formal specifications
+
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).
+
+
+
+
+
λδ version 3 (proposed)
+
+ The formal specification of λδ version 3
+ is forthcoming.
+
-
λδ version 2 (active)
+
λδ version 2 (active)
The formal specification of λδ version 2
is available in the following formats:
@@ -181,9 +256,10 @@
-
-
lambdadelta_2 for Matita 0.99.2
+
lambdadelta_2A1 for Matita 0.99.2
(revised
2014-10).
- Source scripts.
+ Source scripts [Svn revision: 12964].
+
Documentation (R2c).
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).
-
λδ version 1 (superseded)
+ λδ version 1 (superseded)
The formal specification of λδ version 1
is available in the following formats:
@@ -226,10 +289,11 @@
lambdadelta_1 for Coq 7.3.1
- (revised
2015-01).
+ (revised
2015-09).
Source scripts.
+
Documentation (J1a).
- -
+
-
2015 January 15.
17 new lemmas and former lemma "eq_nat_dec" renamed as "nat_dec_neg".
@@ -246,28 +310,28 @@
(revised 2011-09).
Static HTML pages generated by the HELM rendering engine.
+
+ Informational pages on the parts of the specification:
+
Background,
+
Core.
+
-
+
@@ -309,6 +378,6 @@
-
Last update: Fri, 16 Jan 2015 16:47:03 +0100
+
Last update: Fri, 24 Nov 2017 21:00:00 +0100