X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Findex.html;h=317de931de474ab0f75b518235824c941c253c97;hb=e36a0eced135e6f1b79d06c78a408918f65376b6;hp=a224e9df64e98e310fb71ab57688f03e96a3eb83;hpb=c259a5f9cacd93550e80d2195ff4bf68a0d55ddb;p=helm.git diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html index a224e9df6..317de931d 100644 --- a/helm/www/lambdadelta/index.html +++ b/helm/www/lambdadelta/index.html @@ -1,144 +1,207 @@ - - - - - λδ 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 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
+ 		+ specification Dismissed
+ 		+
+ 		+
+ 		+ implementation + +
2
+ 		+ foreword basic_2
+ 		+ milestones April -2011
+ 		+ version 2 planned -in -2013
+ 		+ version 2 not -planned yet
+ 		(background - core - applications) +
+ library + (static LDDL directory)
1
+ 		+ citations + + visibility basic_1
+ 		+ version 1 May -2004
+ 		+ version 1 November -2006
+ 		(background - core)(static HELM directory) + helena 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
-
- - \ No newline at end of file + +
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 previous informal material. +
+
+ This is the System logo: crux_177.png + (revised 2012-09). +
+
+ Notice for the user of Internet Explorer. + 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. +
+ +
Citations [spacer] +
+
+ This is a list of publications citing λδ (not including our own). +
+ + + + + + +
+ [Spacer] +
+
+
+
+
+ + [Valid XHTML 1.1] + + + [Valid CSS level 2] + + + [Generated from XML via XSL] + + + [PNG used here] + + + [Viewable with any browser] + +
+
+
+
+
Last update: Sat, 21 Feb 2015 23:38:38 +0100
+ +