The Formal System λδ (\lambda\delta)
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 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.
version |
name |
developed with |
stage |
started |
announced |
released |
concluded |
Version 2
|
"basic_2" |
Matita 0.99.2
|
"A" |
April 2011 |
June 2014 |
October 2014 |
|
Abandoned |
|
Coq 7.3.1
|
|
March 2008 |
|
|
February 2011 |
Version 1
|
"basic_1" |
Coq 7.3.1
|
|
May 2004 |
December 2005 |
November 2006 |
May 2008 |
λδ version 2 (active)
The formal specification of λδ version 2
is available in the following formats:
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:
Last update: Sat, 01 Nov 2014 17:50:21 +0100