X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fspecification.html;h=b86e965c0073796c78a4fb8548503f933ab670d8;hb=9b1b59a049935f5382ed7def91b807bbf9453894;hp=08b7ec7bdd84b8011dec9363c234a74d4703961b;hpb=4e961fd767a9800fe35fda629f7a2f119d4b165f;p=helm.git diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html index 08b7ec7bd..b86e965c0 100644 --- a/helm/www/lambdadelta/specification.html +++ b/helm/www/lambdadelta/specification.html @@ -16,14 +16,14 @@
- [lambdadelta home] + [\lambda\delta home]
-
The Formal System λδ (\lambda\delta)
+
The Formal Systems of the λδ (\lambda\delta) Family
- [Spacer] + [Spacer]
-
+

@@ -31,206 +31,329 @@ - home + home news + + specification + + +
+ + +
+ documentation - specification + implementation - +
- - implementation - - foreword + foreword milestones + + version 2 + + (background - core - applications) + +
+ version 2 - version 2 + helena - (background - core - applications) - - library + + Open Symbolic Notation (OSN) - notice + citations visibility + + version 1 + + (background - core) + (static HELM directory) version 1 - version 1 - - -
- - - helena + library + (static LDDL directory)
- -
Computer-checked formal specifications [spacer] +
Computer-checked formal specifications [butterfly]
-
- λδ 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, + 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 namedeveloped with stagedeveloped with started announced releaseddismissedconcludedreferences
+ 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 2014Planned in October 2014In progressOctober 2014August 2015 + V2a + R2c +
Abandoned + + + Coq 7.3.1 + March 2008 + + February 2011
Version 1 "basic_1" Coq 7.3.1 May 2004 December 2005 November 2006May 2008May 2008 + V1a + J1a +
- - - -
- [spacer] λδ version 2 (in progress)
-
+
+ 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). +
    • +
+ +
+ [butterfly] λδ version 3 (proposed)
+
+ The formal specification of λδ version 3 + is forthcoming. +
+ +
+ [butterfly] λδ version 2 (active)
+
The formal specification of λδ version 2 is available in the following formats:
- -