From 158da000d9934317055becd9c221c15395970982 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 2 Dec 2012 12:28:43 +0000 Subject: [PATCH] some corrections to the prose of the web site --- helm/www/lambdadelta/documentation.html | 34 +++++++++++++----------- helm/www/lambdadelta/implementation.html | 11 ++++---- helm/www/lambdadelta/index.html | 7 ++--- helm/www/lambdadelta/news.html | 5 ++-- 4 files changed, 31 insertions(+), 26 deletions(-) diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index 0bb864a9c..425084d70 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -1,6 +1,7 @@ + λδ home page @@ -38,7 +39,7 @@ Currently the main source of information on λδ (version 1) is Resource - 1.1 below.
+ 1.9 below.
A summary of basic λδ (version 1) is found in Resource @@ -50,7 +51,7 @@ - - - -
2.1.
+ 		2.4.
 F. Guidi: An @@ -65,7 +66,7 @@
2.2.
+ 		2.3.
 F. Guidi: @@ -89,7 +90,7 @@ Guidi:
2.3.
+ 		2.2.
 F. Guidi: An @@ -105,7 +106,7 @@ Guidi:
2.4.
+ 		2.1.
 F. Guidi: A @@ -127,7 +128,7 @@ Guidi: - - - - - - - -
1.1.
+ 		1.9.
 F. Guidi: @@ -145,7 +146,7 @@ Guidi:
1.2.
+ 		1.8.
 F. Guidi: Lambda @@ -170,7 +171,7 @@ Guidi:
1.3.
+ 		1.7.
 F. Guidi: Lambda Types on @@ -187,7 +188,7 @@ Guidi:
1.4.
+ 		1.6.
 F. Guidi: Lambda @@ -212,7 +213,7 @@ Guidi: F. Guidi: The Formal - System lambdadelta + System λδ (2008-10). Presentation at "Advances in Constructive Topology and Logical @@ -221,7 +222,7 @@ Guidi:
1.6.
+ 		1.4.
 F. Guidi: Towards @@ -236,7 +237,7 @@ Guidi:
1.7.
+ 		1.3.
 F. Guidi: Lambda @@ -251,7 +252,7 @@ Guidi:
1.8.
+ 		1.2.
 F. Guidi: Lambda @@ -269,7 +270,7 @@ Guidi:
1.9.
+ 		1.1.
 F. Guidi: @@ -291,10 +292,11 @@ Guidi:
[Valid HTML 4.01 Transitional] [Use Any - Browser Here] [PNG Used Here]
+ Browser Here]" title="Use Any Browser Here" src="images/globe_trans.png" style="border: 0px solid ; width: 147px; height: 42px;"> [PNG Used Here]

- Last update 2012-12-01 by Ferruccio + Last update 2012-12-02 by Ferruccio Guidi
+ \ No newline at end of file diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index 0163d01c4..e5ecc5760 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -1,6 +1,7 @@ + λδ home page @@ -106,7 +107,7 @@
  • F. Guidi: lambdadelta_1 - (revised 2011-09). + (revised 2012-10). Formal specification for Coq 7.3.1 @@ -129,8 +130,8 @@ Formal
    • A Jed mode @@ -245,7 +246,7 @@ computer Transitional" src="http://www.w3.org/Icons/valid-html401" style="border: 0px solid ; width: 88px; height: 31px;"> [Use Any Browser Here] [PNG Used Here]

      - Last update 2012-12-01 by Ferruccio + Last update 2012-12-02 by Ferruccio Guidi
      diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html index a224e9df6..45fd133bb 100644 --- a/helm/www/lambdadelta/index.html +++ b/helm/www/lambdadelta/index.html @@ -2,6 +2,7 @@ + λδ home page @@ -37,7 +38,7 @@ 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 +enjoying a well-conceived theory, which includes the commonly desired properties.

      λδ takes some features from the calculi of the Automath family and @@ -53,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 @@ -137,7 +138,7 @@ 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 +Last update 2012-12-02 by Ferruccio Guidi
      diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index 8ca8c771d..1c2054123 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -2,6 +2,7 @@ + λδ home page @@ -115,7 +116,7 @@ for Matita 0.5 of the May 2008. The -specification of λδ version 1 is closed.
      +specification of λδ version 1 is dismissed.