+
λδ is developed as a machine-checked digital specification.
It comes in several versions 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 +115,7 @@
Delta:
after its conclusion, the specification is modified just for maintenance.
-
+
-
-
-
-
+
+
λδ version 2 (active)
-
+
The formal specification of λδ version 2
is available in the following formats:
-
-
+
-
-
-
lambdadelta_2 for Matita 0.99.2
+
+
lambdadelta_2 for Matita 0.99.2
(revised
2014-10).
Source scripts.
-
+
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)
-
+
The formal specification of λδ version 1
is available in the following formats:
-
-