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

@@ -31,23 +31,23 @@ - home + home news - - documentation - - + specification - +
- +
+ + documentation + implementation @@ -57,57 +57,56 @@ - foreword + foreword milestones - - version 2 - - + version 2 - (background - core - applications) - + (background - core - applications) +
+ + version 2 + - library + helena + + + Open Symbolic Notation (OSN) - (static LDDL directory) - citations + citations visibility + + version 1 + + (background - core) + (static HELM directory) version 1 - version 1 - - (core) - (static HELM directory) - - 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. @@ -128,52 +127,94 @@ version name - developed with stage + developed with started announced released - concluded + concluded + references + + + + 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 2014 October 2014 - + August 2015 + + V2a + R2c + Abandoned + Coq 7.3.1 - March 2008 - February 2011 + February 2011 + Version 1 "basic_1" + Coq 7.3.1 - May 2004 December 2005 November 2006 - May 2008 + May 2008 + + V1a + J1a + @@ -181,7 +222,7 @@
Informational pages on the specifications are provided.
-
The formal specification of λδ version 2 is available in the following formats: @@ -208,9 +256,10 @@
The formal specification of λδ version 1 is available in the following formats: @@ -240,10 +289,11 @@
  • lambdadelta_1 for Coq 7.3.1 - (revised 2015-01). + (revised 2015-09). Source scripts. + Documentation (J1a).
    - [Spacer] + [Spacer]

    @@ -327,6 +378,6 @@

    -
    Last update: Tue, 20 Jan 2015 18:39:00 +0100
    +
    Last update: Fri, 24 Nov 2017 21:00:00 +0100