From 5924405e7f361a8b2bf638e6a361f7f16cdc7ac2 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 24 Feb 2012 18:21:09 +0000 Subject: [PATCH] site update --- helm/www/lambda_delta/documentation.html | 675 +++++++++++----------- helm/www/lambda_delta/implementation.html | 600 ++++++++++--------- helm/www/lambda_delta/news.html | 413 ++++++------- 3 files changed, 877 insertions(+), 811 deletions(-) diff --git a/helm/www/lambda_delta/documentation.html b/helm/www/lambda_delta/documentation.html index 64120aa00..2ff59112b 100644 --- a/helm/www/lambda_delta/documentation.html +++ b/helm/www/lambda_delta/documentation.html @@ -1,80 +1,86 @@ - + - - - lambda_delta home page - - - - - -
-
-[Crux Logo] -

The Formal System λδ (lambda_delta)
-

-

Towards the unification of terms, types, environments and contexts

-[Separator]
- - - - - - - -
- - -
    -
  • Papers
    • -
- - 		-

Documentation [Butterfly]

-Currently the main source of -information on λδ (version 1) is Resource -1.1 below.
-A summary of basic λδ (version -1) is found in Resource 1.5 -below.
-

[Basic lambda_delta Logo] Basic λδ version 2 (in progress):

- + + + lambda_delta home page + + + + + +
+
+ [Crux Logo] +

The Formal System λδ (lambda_delta)
+

+

Towards the unification of terms, types, environments and + contexts

+ [Separator]
+
- - - - - -
2.1.
+ 		+ + +
    +
  • Papers
    • +
+ 		F. Guidi: An -Efficient -Validation Procedure for the Formal System λδ -(2010-07). In CiE 2010 Local Proceedings. -University of Azores, CMATI Booklet, pp. 204-213. BibTeX entry.
-
-
2.2.
- 		F. + +

Documentation [Butterfly]

+ Currently the main + source of + information on λδ (version 1) is Resource + 1.1 below.
+ A summary of + basic λδ (version + 1) is found in Resource + 1.5 + below.
+

[Basic + lambda_delta Logo] Basic λδ version 2 (in + progress):

+ + + + + + + + + - - - - - - - - - - -
2.1.
+ 		F. + Guidi: An + Efficient + Validation Procedure for the Formal System λδ + (2010-07). + In CiE 2010 + Local Proceedings. + University of Azores, CMATI Booklet, pp. 204-213. + BibTeX entry.
+
+
2.2.
+ 		F. Guidi: @@ -86,277 +92,264 @@ Guidi: - Landau's -"Grundlagen der Analysis" from Automath to lambda-delta (2009-09). University of -Bologna, technical report UBLCS-2009-16. BibTeX entry.
-
-
2.3.
- 		F. Guidi: An -Efficient -Validation Procedure for the Formal System λδ (2010-07). Presentation -at -CiE -2010 -(slides).
-
-
2.4.
- 		F. Guidi: A -Validator -for the Formal System λδ (revised 2010-02). Presentation -at -the -University -of -Bologna -(slides).
-

[Basic lambda_delta Logo] Basic λδ version 1 (closed):

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + +
1.1.
- 		F. -Guidi: The Formal System λδ (2009-10). In ACM ToCL 11(1), Article -No. 5 (accepted - 2008-07). CoRR -identifier cs/0611040 [v10] (revised 2008-09). BibTeX -entry.
-
-
1.2.
- 		F. Guidi: Lambda -Types on the Lambda Calculus with -Abbreviations (2007-06). -In - - - - - - - - - - - - - - - CiE 2007 Local Proceedings. -University -of -Siena, -technical -report -487, -p. -387 -(abstract -of -a -presentation). - - - - - - - - - BibTeX -entry.
-
-
1.3.
- 		F. Guidi: Lambda Types on the Lambda Calculus with -Abbreviations (2006-11). -University -of -Bologna, -technical -report -UBLCS-2006-25. - - - - - - - - - - - - - - - - BibTeX -entry.
-
-
1.4.
- 		F. Guidi: Lambda -Types -on -the -Lambda -Calculus -with -Abbreviations: -a -Certified -Specification (2006-01). -University of -Bologna, technical report UBLCS-2006-01. BibTeX entry.
-
-
1.5.
- 		F. Guidi: The -Formal -System lambda-delta -(2008-10). Presentation at -"Advances in Constructive Topology and Logical Foundations" (slides).
-
-
1.6.
- 		F. Guidi: Towards -the Unification of Terms, Types -and Contexts (2008-03). -Presentation -at -Types -2008 -(slides).
-
-
1.7.
- 		F. Guidi: Lambda -Types on the Lambda Calculus with -Abbreviations (2007-06). -Presentation -at -CiE -2007 -(slides).
-
-
1.8.
- 		F. Guidi: Lambda -Tipi sul Lambda Calcolo con -Abbreviazioni (2007-01). -Presentation -at -the -University -of -Padova -(slides - - - - - - - - in -Italian).
-
-
1.9.
- 		F. -Guidi: Lambda Tipi sul Lambda Calcolo con -Abbreviazioni: una Specifica Certificata (2005-12). Presentation at -the University of Bologna (slides in -Italian).
+ Landau's + "Grundlagen der Analysis" from Automath to + lambda-delta (2009-09). + University of + Bologna, technical report UBLCS-2009-16. BibTeX entry.
+
+
2.3.
+ 		F. + Guidi: An + Efficient + Validation Procedure for the Formal System λδ + (2010-07). + Presentation + at + CiE + 2010 + (slides).
+
+
2.4.
+ 		F. + Guidi: A + Validator + for the Formal System λδ (revised 2010-02). + Presentation + at + the + University + of + Bologna + (slides).
+

[Basic + lambda_delta Logo] Basic λδ version 1 + (closed):

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
1.1.
+ 		F. +Guidi: + The Formal System + λδ (2009-10). In ACM ToCL 11(1), + Article + No. 5 (accepted + 2008-07). + CoRR + identifier cs/0611040 + [v10] (revised 2008-09). + BibTeX + entry.
+
+
1.2.
+ 		F. + Guidi: Lambda + Types on the Lambda Calculus with + Abbreviations (2007-06). + In CiE 2007 + Local Proceedings. + University + of + Siena, + technical + report + 487, + p. + 387 + (abstract + of + a + presentation). BibTeX + entry.
+
+
1.3.
+ 		F. + Guidi: Lambda Types on + the Lambda Calculus with + Abbreviations (2006-11). + University + of + Bologna, + technical + report + UBLCS-2006-25. BibTeX + entry.
+
+
1.4.
+ 		F. + Guidi: Lambda + Types + on + the + Lambda + Calculus + with + Abbreviations: + a + Certified + Specification (2006-01). + University of + Bologna, technical report UBLCS-2006-01. BibTeX entry.
+
+
1.5.
+ 		F. + Guidi: The + Formal + System lambda-delta + (2008-10). + Presentation at + "Advances in Constructive Topology and Logical + Foundations" (slides).
+
+
1.6.
+ 		F. + Guidi: Towards + the Unification of Terms, Types + and Contexts (2008-03). + Presentation + at + Types + 2008 + (slides).
+
+
1.7.
+ 		F. + Guidi: Lambda + Types on the Lambda Calculus with + Abbreviations (2007-06). + Presentation + at + CiE + 2007 + (slides).
+
+
1.8.
+ 		F. + Guidi: Lambda + Tipi sul Lambda Calcolo con + Abbreviazioni (2007-01). + Presentation + at + the + University + of + Padova + (slides in + Italian).
+
+
1.9.
+ 		F. +Guidi: + Lambda Tipi sul + Lambda Calcolo con + Abbreviazioni: una Specifica Certificata + (2005-12). + Presentation at + the University of Bologna (slides in + Italian).
+
-
-
-[Valid HTML 4.01 Transitional] [Use Any Browser Here] [PNG Used Here]
-
-Last update 2012-02-21 by Ferruccio -Guidi
-
- +
+ [Valid HTML 4.01 Transitional] [Use Any + Browser Here] [PNG Used Here]
+
+ Last update 2012-02-24 by Ferruccio + Guidi
+ + diff --git a/helm/www/lambda_delta/implementation.html b/helm/www/lambda_delta/implementation.html index 79f013900..8d16e6890 100644 --- a/helm/www/lambda_delta/implementation.html +++ b/helm/www/lambda_delta/implementation.html @@ -1,281 +1,327 @@ - + - - - lambda_delta home page - - - - - -
-
-[Crux Logo] -

The Formal System λδ (lambda_delta)
-

-

Towards the unification of terms, types, environments and contexts

-[Separator]
- - - - - + + +
- - - -
    -
  • Resources
    -
    • -
- 		-

Computer-checked formal -specifications [Butterfly]

- Resource -1 below provides for the statically generated natural language representation of -λδ meta-theory (faster rendering w.r.t. resource 2 below).
- Resource 2 below provides -for the dynamically generated natural -language representation of -λδ meta-theory (powered by the HELM -rendering engine).
-Remarkably, λδ was born and developed in the digital format of resource 3 below, which is not the -formal counterpart of some informal material previously written on -paper (as it happens for most currently digitalized Mathematics).
-
    -
  1. F. Guidi: lambda_delta -(revised 2011-09). Formal -specification for Matita 0.5 -(HTML pages generated -by the HELM -rendering engine)
    -Here are the most relevant theorems proved in the formal specification: - -
    2. -
  2. F. Guidi: lambda_delta -(revised 2011-09). Formal -specification for Matita 0.5 (HELM directory).
    -
    -
    3. -
  3. F. Guidi: lambda_delta_1 -(revised 2011-09). -Formal specification for Coq 7.3.1 -(source -proof scripts). BibTeX entry.
    -
    4. -
-

Tools [Butterfly]

- [Crux Logo] The λδ -Digital -Library -(LDDL) is part of HELM -and contains a set of -resources expressed in λδ.
-
    -
  • Contents: Landau's "Grundlagen der Analysis" (from -Jutting's specification in Automath).
    -
    • -
- - + + + lambda_delta home page + + + + + +

- [Helena Logo] Helena is a λδ -processor, -implemented in Caml as a part of -the HELM software, meant for -testing the stable features of the calculus as well as the unstable -ones.
-The processor source code is available in the directory /trunk/helm/software/helena/ -of the HELM Svn -repository. The Svn revisions containing the stable versions -of  Helena are indicated below.
-
    -
-
    -
  • Version 0.8.2. In -progress.
    -
    • -
-
    -
  • Version 0.8.1 (2010-11). -Exploits a subset of "complete_rg" λδ as the intermediate language. -Features importation from ".hln" files containing λδ textual syntax. -The overall validation speed of the "Grundlagen -der -Analysis" increases of 22% with respect to version 0.8.0. [Svn -revision: 11032] (archived -source code) -
      -
    • 2009-12. Helena -appears in F. Wiedijk's index + [Crux Logo] +

      The Formal System λδ (lambda_delta)
      +

      +

      Towards the unification of terms, types, environments and + contexts

      + [Separator]
      + + + + + - - -
      + + + +
        +
      • Resources
        +
        • +
      +       		+

      Computer-checked formal + specifications [Butterfly]

      + Resource + 1 below provides for the statically generated natural language + representation of + λδ meta-theory (faster rendering w.r.t. resource 2 below).
      + Resource 2 below + provides + for the dynamically generated natural + language representation of + λδ meta-theory (powered by the HELM + rendering engine).
      + Remarkably, λδ was born and developed in the digital + format of resource 3 + below, which is not the + formal counterpart of some informal material previously + written on + paper (as it happens for most currently digitalized + Mathematics).
      +
        +
      1. F. Guidi: lambda_delta + (revised 2011-09). + Formal + specification for Matita 0.5 + (HTML pages generated + by the HELM + rendering engine)
        + Here are the most relevant theorems proved in the + formal specification: + +
        2. +
      2. F. Guidi: lambda_delta + (revised 2011-09). + Formal + specification for Matita 0.5 (HELM directory).
        +
        +
        3. +
      3. F. Guidi: lambda_delta_1 + (revised 2011-09). +Formal + specification for Coq + 7.3.1 + (source + proof scripts). BibTeX entry.
        +
        4. +
      +

      Tools [Butterfly]

      + [Crux Logo] The λδ + Digital + Library + (LDDL) is part of HELM + and contains a set of + resources expressed in λδ.
      +
        +
      • Contents: + Landau's "Grundlagen + der Analysis" (from + Jutting's specification in Automath).
        +
        • +
      + + +
      + [Helena Logo] Helena + is a λδ + processor, + implemented in Caml + as a part of + the HELM software, + meant for + testing the stable features of the calculus as well as the + unstable + ones.
      + The processor source code is available in the directory /trunk/helm/software/helena/ + of the HELM + Svn + repository. The Svn revisions containing the stable + versions + of  Helena are indicated below.
      +
        +
      +
        +
      • Version 0.8.2. + In + progress.
        +
        • +
      +
        +
      • Version 0.8.1 + (2010-11). + Exploits a subset of "complete_rg" λδ as the + intermediate language. + Features importation from ".hln" files containing λδ + textual syntax. + The overall validation speed of the "Grundlagen + der + Analysis" increases of 22% with respect to + version 0.8.0. [Svn + revision: 11032] (archived + source code) + -
        • -
      -
        -
      • Version 0.8.0 (2009-09). Supports -"basic_rg" λδ with naive implementation of impredicative sort -inclusion. Features -importation from Automath -and exportation to XML. [Svn -revision: 10304] (archived -source code)
        -
          -
        • 2009-09. -Jutting's specification of Landau's "Grundlagen -der -Analysis" enters λδ Digital Library.
          -
          • -
        • 2009-06. -Jutting's specification of Landau's "Grundlagen -der -Analysis" is -successfully processed, enabling sort inclusion.
          • -
        -
        • -
      -

      Other resources [Butterfly]

      - -
        -
      • A Jed mode for -editing ".hln" files (containing λδ textual syntax): helena.sl -(revised 2010-11).
        • -
      - -
        -
      • A logo for "basic" λδ: bld.pdf (revised 2008-07).
        -
        • -
      -
      -
      -[Valid HTML 4.01 Transitional] [Use Any Browser Here] [PNG Used Here]
      -
      -Last update 2012-02-21 by Ferruccio -Guidi
      -
- +computer + math systems. + + + +
    +
  • Version 0.8.0 (2009-09). + Supports + "basic_rg" λδ with naive implementation of + impredicative sort + inclusion. Features + importation from Automath + and exportation to XML. + [Svn + revision: 10304] (archived + source code)
    +
      +
    • 2009-09. + Jutting's specification of Landau's "Grundlagen + der + Analysis" enters λδ Digital Library.
      +
      • +
    • 2009-06. + Jutting's specification of Landau's "Grundlagen + der + Analysis" is + successfully processed, enabling sort inclusion.
      • +
    +
    • +
+

Other resources [Butterfly]

+ +
    +
  • A Jed mode + for + editing ".hln" files (containing λδ textual syntax): helena.sl + (revised 2010-11).
    • +
+ +
    +
  • A logo for "basic" λδ: bld.pdf + (revised 2008-07).
    +
    • +
+
+
+ [Valid HTML 4.01 Transitional] [Use Any + Browser Here] [PNG Used Here]
+
+ Last update 2012-02-24 by Ferruccio + Guidi
+
+ diff --git a/helm/www/lambda_delta/news.html b/helm/www/lambda_delta/news.html index aecc87973..388833406 100644 --- a/helm/www/lambda_delta/news.html +++ b/helm/www/lambda_delta/news.html @@ -1,140 +1,158 @@ - + - - - lambda_delta home page - - - - - -
-
-[Crux Logo] -

The Formal System λδ (lambda_delta)
-

-

Towards the unification of terms, types, environments and contexts

-[Separator]
- - - - - - - -
- -
    -
  • News
    • -
- - - 		-

News [Butterfly]

-
    -
  • September 2011. The -denomination "lambda-delta" changes to "lambda_delta".
    • -
      -
    • The character "-" is reserved in λδ textual syntax -(recognized by Helena 0.8.1).
      -
      • -
    • Eventually, the occurrences of the character "-" will be -replaced by "_" in all λδ-related identifiers.
      • -
    • In particular, this refactoring involves file names and -path names.
      • -
    • The permanent λδ URL is sheduled to become http://lambda_delta.info on -December 2012.
      -
      • -
    -
-
    -
  • April 2011. The -specification of λδ version 2 and related topics is restarted in Matita 0.5.
    • -
      -
    • Here is a page about the -specification (Core).
      -
      • -
    • Here is a page about the -topics related to the specification (Applications).
      -
      • -
    -
- -
    -
  • November 2010. Helena 0.8.1 is released.
    -
    • -
- - - -
    -
  • September 2008. -This site is online.
    -
    • -
- - - - -
    -
  • March 2008. The -specification of λδ version 2 is started with Coq 7.3.1 (false start). -
    • -
- - - -

Visibility [Butterfly]

-
    -
  • February 2012. -The Google -search for formal system lambda -delta -gives 5 resources about λδ in the first 6 results.
    -
    • -
-
    -
  • February 2012. -The Yahoo -search formal system lambda delta -gives this site as the first result.
    • -
-
-
-[Valid HTML 4.01 Transitional] [Use Any Browser Here] [PNG Used Here]
-
-Last update 2012-02-24 by Ferruccio -Guidi
-
- + + + + + +

Visibility [Butterfly]

+ + + + + + +
+ [Valid HTML 4.01 Transitional] [Use Any + Browser Here] [PNG Used Here]
+
+ Last update 2012-02-24 by Ferruccio + Guidi
+ + -- 2.39.2