X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Findex.html;h=190bf2ebbe0b21f2268d7a61a497ae83e4e4e7fe;hb=9b75ad80a3ee31314c02f113b255ad533a87d3d2;hp=fc46d7254ae8612578e4a3d090d26b9761346eb4;hpb=2a5e0b799cd6aae5d920c67a5ddc9d9888cf7e80;p=helm.git diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html index fc46d7254..190bf2ebb 100644 --- a/helm/www/lambdadelta/index.html +++ b/helm/www/lambdadelta/index.html @@ -1,179 +1,140 @@ - - - - - lambdadelta home page - - - - - -
-
-[Crux Logo] -

The Formal System λδ (lambdadelta)
-

-

Towards the unification of terms, types, environments and contexts

-[Separator]
- - - - - - - -
-
    -
  • Foreword
    • -
- - - - 		-

Foreword [Butterfly]

-The formal system λδ -(lambdadelta) 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 -desired properties.
-
-λδ takes some features from the calculi of the Automath family and -some from the pure type systems, but it differs from both in that it -does not include the Π construction while it provides for an -abbreviation mechanism at the level of terms.
-
-λδ features explicit type annotations, which are borrowed from -realistic type checker implementations and with which type checking is -reduced to type inference.
-
-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 -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 -decidability of type inference and of type checking come as corollaries.
-
-λδ features uniformly dependent types and a predicative abstraction -mechanism, so the calculus can serve as a formal specification language -for the type theories that need a predicative foundation. λδ is -expected to have the expressive power of λ→.
-
-λδ comes in several versions listed in the following table, which -includes the major milestones:
-
- + + + + + + + + + + \lambda\delta home page + + + + + + +
+ + [lambdadelta home] + +
+
The Formal System λδ (\lambda\delta)
+
+ [Spacer] +
+
+
+
+
+
- - - - - + - - - - - + - - - - -
Version
+ 		+ home Name
+ 		+ news Started
+ 		+ documentation Released
- 		Dismissed
+ 		+ implementation (specifications - library - Helena)
2
- 		basic_2
+ 		+ Foreword April -2011
+ 		+ Milestones planned -in -2013
+ 		+ Version 2 not -planned yet
+ 		+ Version 2 (Background - Core - Applications)
1
+ 		+ Notice basic_1
+ 		+ Visibility May -2004
+ 		+ Version 1 November -2006
+ 		+ Version 1 May -2008
+ 		+
-
-

Notice -for -the -Internet -Explorer -user [Butterfly]

-To view this site -correctly, please select a font with Unicode -support. -For example Lucida Sans Unicode -(it should be already installed on your system). -To change the current font follow: "Tools" -menu -→ "Internet -Options" entry → "General" tab → "Fonts" button.
-
-
-[Valid HTML 4.01 Transitional] [Use Any Browser Here] [PNG Used Here]
-
-Last update 2012-12-01 by Ferruccio -Guidi
-
+ + +
Foreword [spacer] +
+
+ The formal system λδ (\lambda\delta) is a typed λ-calculus aiming to support + the foundations of Mathematics that require an underlying specification language + (for example the Minimal Type Theory + and its predecessors). +
+
+ λδ is developed in the context of the + Hypertextual Electronic Library of Mathematics + as a machine-checked digital specification + that is not the formal counterpart of some previously published informal material. +
+
+ This is the System logo: crux_177.png + (revised 2012-09). +
+ +
Notice for the Internet Explorer user [spacer] +
+
+ To view this site correctly, please select a font + with Unicode support. + For example "Lucida Sans Unicode" (it should be already installed on your system). + To change the current font follow: + "Tools" menu → "Internet Options" entry → "General" tab → "Fonts" button. +
+ +
+ [Spacer] +
+
+
+
+
+ + [Valid XHTML 1.1] + + + [Valid CSS level 2] + + + [Generated from XML via XSL] + + + [PNG used here] + + + [Viewable with any browser] + +
+
+
+
+
Last update: Sun, 05 Oct 2014 16:38:32 +0200