The Formal Systems of the λδ (\lambda\delta) Family
Computerchecked formal specifications
The systems of the λδ family are developed as machinechecked 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,
then the calculus is announced with a presentation.
Beta:
major changes and additions may occur before the calculus is released on paper.
Gamma:
subsequent improvements occur until the specification is completed or superseded,
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(12), Springer (February 2010), pp. 5378].

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:
Informational pages on the parts of the specification:
Background,
Syntax,
Core,
Applications.
λδ version 1 (superseded)
The formal specification of λδ version 1
is available in the following formats:
Informational pages on the parts of the specification:
Background,
Core.
Last update: Wed, 14 Nov 2018 18:50:48 +0100