- λδ 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,180 +121,239 @@
Delta:
after its conclusion, the specification is modified just for maintenance.
-
+
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
+ |
-
-
-
-
-
λδ version 2 (active)
-
+
+ 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)
+
The formal specification of λδ version 2
is available in the following formats:
-
-
+
-
-
-
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.
-
-
Notice:
+
+
Notice:
the scripts are checked by the latest version of Matita from
HELM Subversion repository
at path <trunk/matita/>.
-
+
-
-
+
Informational pages on the parts of the specification:
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:
-
-
+
-
-
-
lambdadelta_1 for Coq 7.3.1
- (revised
2012-10).
+
+
lambdadelta_1 for Coq 7.3.1
+ (revised
2015-09).
Source scripts.
-
-
+
Documentation (J1a).
+
+ -
+ 2015 January 15.
+ 17 new lemmas and former lemma "eq_nat_dec" renamed as "nat_dec_neg".
+
+
+
+
The scripts are grouped in directories, one for each part.
-
+
-
-
+
-
-
+
-
-
-
+
+ Informational pages on the parts of the specification:
+
Background,
+
Core.
+
+
+
@@ -309,6 +378,6 @@
-
Last update: Tue, 04 Nov 2014 16:21:22 +0100
-
+
Last update: Fri, 24 Nov 2017 21:00:00 +0100
+