- λδ is developed as a machine-checked digital specification.
- It comes in several versions listed in the next table,
- which includes the major milestones.
-
-
+\lambda\delta home page
The Formal Systems of the λδ (\lambda\delta) Family
+ 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,
@@ -114,195 +15,71 @@
while major changes and additions are announced and reported on paper.
Delta:
after its conclusion, the specification is modified just for maintenance.
-
+ 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:
-
- 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:
-