Version + | + foreword | -Name + | + news | -Started + | + documentation | -Released - |
- Dismissed + | + implementation |
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fwww%2Flambdadelta%2Findex.html;h=ce113aff0abfce082ff3ada820e6c1d18520ccf4;hb=c0d87c3cdf879f61aa53e91f43580e9815ae7190;hp=07e98c6a926e9ec182be6d56c1ff5853404fd173;hpb=22d35425b8f5f7e479db3be59b73f76d77ae6711;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 @@ - -
- - - -
-
|
-
- Foreword
-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: - -
Foreword
+ ![]()
+ 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:
+
+
+
- Notice
-for
-the
-Internet
-Explorer
-user
-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.- - - - - ![]() ![]() - -Last update 2014-02-24 by Ferruccio -Guidi - + + + + Notice for the Internet Explorer user
+ ![]()
+ 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.
+
-
+
+
+ ![]()
+
+
+ +
+
+ + Last update: Sun, 06 Jul 2014 16:37:09 +0200
+
+
|