X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Findex.html;h=62e31753bd6040f68e34993f50db81b7756ddbd8;hb=b2c1a95861424ba23e491e2b258f7413efbc1fba;hp=fc46d7254ae8612578e4a3d090d26b9761346eb4;hpb=2a5e0b799cd6aae5d920c67a5ddc9d9888cf7e80;p=helm.git diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html index fc46d7254..62e31753b 100644 --- a/helm/www/lambdadelta/index.html +++ b/helm/www/lambdadelta/index.html @@ -1,26 +1,21 @@ - - - - lambdadelta home page + + + + + λδ home page + - - - - + +

-[Crux Logo] -

The Formal System λδ (lambdadelta)
+[Crux Logo] +

The Formal System λδ (\lambda\delta)

Towards the unification of terms, types, environments and contexts

-[Separator]
- +[Separator]
+
@@ -39,13 +34,11 @@ -

Foreword [Butterfly]

+

Foreword [Butterfly]

The formal system λδ -(lambdadelta) is a typed lambda calculus that pursues the static and +(\lambda\delta) is a typed lambda calculus that pursues the static and dynamic unification of terms, types, environments and contexts while -enjoying a well-conceived meta-theory, which includes the commonly +enjoying a well-conceived theory, which includes the commonly desired properties.

λδ takes some features from the calculi of the Automath family and @@ -61,7 +54,7 @@ The reduction steps of λδ include β-contraction, δ-expansion, ζ-contraction and θ-swap. On the other hand, η-contraction is not included.

-The meta-theory of λδ includes important properties such as the +The theory of λδ includes important properties such as the confluence of reduction, the correctness of types, the uniqueness of types up to conversion, the subject reduction of the type assignment, the strong normalization of the typed terms. The @@ -75,64 +68,48 @@ expected to have the expressive power of λ→.
λδ comes in several versions listed in the following table, which includes the major milestones:

- +
- - - - - - - - - - - - - - - @@ -144,8 +121,7 @@ for the Internet Explorer -user [Butterfly] +user [Butterfly] To view this site correctly, please select a font with Unicode support. @@ -160,20 +136,10 @@ Options" entry → "General" tab → "Fonts" button.
Version
+ 		Version
Name
+ 		Name
Started
+ 		Started
Released
+ 		Released
Dismissed
+ 		Dismissed
2
+ 		2
basic_2
+ 		basic_2
April + April 2011
planned + planned in 2013
not + not planned yet
1
+ 		1
basic_1
+ 		basic_1
May + May 2004
November + November 2006
May + May 2008

-[Valid HTML 4.01 Transitional] [Use Any Browser Here] [PNG Used Here]
+[Valid HTML 4.01 Transitional] [Use Any Browser Here] [PNG Used Here]

-Last update 2012-12-01 by Ferruccio +Last update 2012-12-02 by Ferruccio Guidi
- - + +