X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fspecification.html;h=b86e965c0073796c78a4fb8548503f933ab670d8;hb=9b1b59a049935f5382ed7def91b807bbf9453894;hp=2714bff80659e29771e0dc90e64dc6f45eb38833;hpb=03401922e645207c7b64b52e1c4349f7951fcf71;p=helm.git diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html index 2714bff80..b86e965c0 100644 --- a/helm/www/lambdadelta/specification.html +++ b/helm/www/lambdadelta/specification.html @@ -16,12 +16,12 @@

+ $[\lambda\delta home]$

The Formal Systems of the Î»Î´ (\lambda\delta) Family

+ $\lambda\delta rainbow rule$

@@ -31,7 +31,7 @@ - home + home news @@ -57,7 +57,7 @@ - foreword + foreword milestones @@ -73,13 +73,15 @@ version 2 - library + helena + + + Open Symbolic Notation (OSN) - (static LDDL directory) - citations + citations visibility @@ -93,16 +95,14 @@ version 1 - helena - - -
+ library + (static LDDL directory)

Computer-checked formal specifications [spacer]

Computer-checked formal specifications $\lambda\delta butterfly$

The systems of the Î»Î´ family are developed as machine-checked digital specifications, @@ -127,8 +127,8 @@ version name - developed with stage + developed with started announced released @@ -147,7 +147,7 @@ - J3a + J3a @@ -155,17 +155,15 @@ Version 2 "basic_2" + "A2" - Matita 0.99.2 + Matita 0.99.3 - "A2" October 2015 - -
- + @@ -174,50 +172,48 @@
- -
- "A1" + + Matita 0.99.2 + April 2011 June 2014 October 2014 August 2015 - V2a - R2c + V2a + R2c 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 - V1a - J1a + V1a + J1a @@ -245,14 +241,14 @@

Î»Î´ version 3 (proposed)

+ $\lambda\delta butterfly$ Î»Î´ version 3 (proposed)

The formal specification of Î»Î´ version 3 is forthcoming.

Î»Î´ version 2 (active)

+ $\lambda\delta butterfly$ Î»Î´ version 2 (active)

The formal specification of Î»Î´ version 2 is available in the following formats: @@ -262,7 +258,7 @@

lambdadelta_2A1 for Matita 0.99.2 (revised 2014-10). - Source scripts. + Source scripts [Svn revision: 12964]. Documentation (R2c).

@@ -284,7 +280,7 @@

Î»Î´ version 1 (superseded)

+ $\lambda\delta butterfly$ Î»Î´ version 1 (superseded)

The formal specification of Î»Î´ version 1 is available in the following formats: @@ -297,7 +293,7 @@ Source scripts. Documentation (J1a).

+
2015 January 15. 17 new lemmas and former lemma "eq_nat_dec" renamed as "nat_dec_neg".

2011-09

HELM

+
Confluence of reduction (Church-Rosser property).
+
Correctness of types.
+
Uniqueness of types up to conversion.
+
Subject reduction of the type assignment.
+
Strong normalization of the typed terms.
+
Decidability of the type inference problem.

Core

+ $\lambda\delta rainbow rule$

@@ -382,6 +378,6 @@

Last update: Sat, 23 Jan 2016 00:45:18 +0100

Last update: Fri, 24 Nov 2017 21:00:00 +0100