X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Findex.html;h=ce113aff0abfce082ff3ada820e6c1d18520ccf4;hb=c0d87c3cdf879f61aa53e91f43580e9815ae7190;hp=07e98c6a926e9ec182be6d56c1ff5853404fd173;hpb=73445ceb9d6f8a37784d8d2c73dabe800c6e0926;p=helm.git diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html index 07e98c6a9..ce113aff0 100644 --- a/helm/www/lambdadelta/index.html +++ b/helm/www/lambdadelta/index.html @@ -1,145 +1,146 @@ - - - - - - λδ home page - - - - -
-
-[Crux Logo] -

The Formal System λδ (\lambda\delta)
-

-

Towards the unification of terms, types, environments and contexts

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

Foreword [Butterfly]

-The formal system λδ -(\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 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 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
+ 		+ foreword Name
+ 		+ news Started
+ 		+ documentation Released
- 		Dismissed
+ 		+ implementation
+ + + +
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. +
+
+ λδ comes in several versions listed in the following table, + which includes the major milestones: +
+
+ + - - - - - + + + + + + + - - - + + - - + + + + + + + + + + + +
2
- 		basic_2
- 		April -2011
- 		planned -in -2014
- 		not -planned yet
- 		versionnamedeveloped withstartedannouncedreleaseddismissed
1
- 		basic_1
- 		May -2004
+ 		2basic_2 + Matita 0.99.2 November -2006
- 		May -2008
+ 		April 2011July 2014Planned in 2014Not planned yet
1basic_1 + Coq 7.3.1 May 2004January 2006November 2006May 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 2014-02-24 by Ferruccio -Guidi
-
+ + + +
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, 06 Jul 2014 16:37:09 +0200
+ +