From: Ferruccio Guidi Date: Sat, 1 Dec 2012 22:06:38 +0000 (+0000) Subject: web site update X-Git-Tag: make_still_working~1423 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c259a5f9cacd93550e80d2195ff4bf68a0d55ddb;p=helm.git web site update --- diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index d855689c2..0bb864a9c 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -1,26 +1,21 @@ - - - - lambdadelta home page + + + + λδ home page + - - - - + +

- [Crux Logo] -

The Formal System λδ (lambdadelta)
+ [Crux Logo] +

The Formal System λδ (\lambda\delta)

Towards the unification of terms, types, environments and contexts

- [Separator]
- + [Separator]
+
@@ -39,13 +34,10 @@ -

Documentation [Butterfly]

+

Documentation [Butterfly]

Currently the main source of - information on λδ (version 1) is Resource + information on λδ (version 1) is Resource 1.1 below.
A summary of basic λδ (version @@ -53,22 +45,17 @@ 1.5 below.

[Basic - lambdadelta Logo] Basic λδ version 2 (in + lambdadelta Logo]" title="Basic lambdadelta" src="images/basic_32.png"> Basic λδ version 2 (in progress):

- +
@@ -109,8 +92,7 @@ href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2009.bib?ncstrl.cabernet//BO
2.1.
 F. - Guidi: An + Guidi: An Efficient - Validation Procedure for the Formal System λδ + Validation Procedure for the Formal System λδ (2010-07). In CiE 2010 Local Proceedings. @@ -93,15 +80,11 @@ Guidi: - Landau's + Landau's "Grundlagen der Analysis" from Automath to - lambdadelta (2009-09). + lambda-delta (2009-09). University of - Bologna, technical report UBLCS-2009-16. BibTeX entry.
+ Bologna, technical report UBLCS-2009-16. BibTeX entry.
2.3.
 F. - Guidi: An + Guidi: An Efficient Validation Procedure for the Formal System λδ (2010-07). @@ -126,11 +108,9 @@ href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2009.bib?ncstrl.cabernet//BO 2.4.
 F. - Guidi: A + Guidi: A Validator - for the Formal System λδ (revised 2010-02). + for the Formal System λδ (revised 2010-02). Presentation at the @@ -142,30 +122,22 @@ href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2009.bib?ncstrl.cabernet//BO

[Basic - lambdadelta Logo] Basic λδ version 1 + lambdadelta Logo]" title="Basic lambdadelta" src="images/basic_32.png"> Basic λδ version 1 (dismissed):

- +
@@ -204,19 +173,15 @@ Guidi: @@ -225,8 +190,7 @@ href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2006.bib?ncstrl.cabernet//BO @@ -248,8 +210,7 @@ href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2006.bib?ncstrl.cabernet//BO @@ -336,20 +289,12 @@ Guidi:
1.1.
 F. Guidi: - The Formal System - λδ (2009-10). In ACM ToCL 11(1), + The Formal System + λδ (2009-10). In ACM ToCL 11(1), Article - No. 5 (accepted + No. 5 (accepted 2008-07). CoRR - identifier cs/0611040 + identifier cs/0611040 [v10] (revised 2008-09). BibTeX entry.
@@ -176,11 +148,9 @@ Guidi: 		1.2.
 F. - Guidi: Lambda + Guidi: Lambda Types on the Lambda Calculus with - Abbreviations (2007-06). + Abbreviations (2007-06). In CiE 2007 Local Proceedings. University @@ -194,8 +164,7 @@ Guidi: (abstract of a - presentation). BibTeX + presentation). BibTeX entry.

1.3.
 F. - Guidi: Lambda Types on + Guidi: Lambda Types on the Lambda Calculus with - Abbreviations (2006-11). + Abbreviations (2006-11). University of Bologna, technical report - UBLCS-2006-25. BibTeX + UBLCS-2006-25. BibTeX entry.

1.4.
 F. - Guidi: Lambda + Guidi: Lambda Types on the @@ -236,11 +200,9 @@ href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2006.bib?ncstrl.cabernet//BO Abbreviations: a Certified - Specification (2006-01). + Specification (2006-01). University of - Bologna, technical report UBLCS-2006-01. BibTeX entry.
+ Bologna, technical report UBLCS-2006-01. BibTeX entry.
1.5.
 F. - Guidi: The + Guidi: The Formal System lambdadelta (2008-10). @@ -263,11 +224,9 @@ href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2006.bib?ncstrl.cabernet//BO 1.6.
 F. - Guidi: Towards + Guidi: Towards the Unification of Terms, Types - and Contexts (2008-03). + and Contexts (2008-03). Presentation at Types @@ -280,11 +239,9 @@ href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2006.bib?ncstrl.cabernet//BO 1.7.
 F. - Guidi: Lambda + Guidi: Lambda Types on the Lambda Calculus with - Abbreviations (2007-06). + Abbreviations (2007-06). Presentation at CiE @@ -297,11 +254,9 @@ href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2006.bib?ncstrl.cabernet//BO 1.8.
 F. - Guidi: Lambda + Guidi: Lambda Tipi sul Lambda Calcolo con - Abbreviazioni (2007-01). + Abbreviazioni (2007-01). Presentation at the @@ -318,14 +273,12 @@ href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2006.bib?ncstrl.cabernet//BO F. Guidi: - Lambda Tipi sul + Lambda Tipi sul Lambda Calcolo con Abbreviazioni: una Specifica Certificata (2005-12). Presentation at - the University of Bologna (slides in + the University of Bologna (slides in Italian).

- [Valid HTML 4.01 Transitional] [Use Any - Browser Here] [PNG Used Here]
+ [Valid HTML 4.01 Transitional] [Use Any + Browser Here] [PNG Used Here]

- Last update 2012-12-01 by Ferruccio + Last update 2012-12-01 by Ferruccio Guidi
- - + + \ No newline at end of file diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index 67872e9d6..0163d01c4 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -1,26 +1,21 @@ - - - - lambdadelta home page + + + + λδ home page + - - - - + +

- [Crux Logo] -

The Formal System λδ (lambdadelta)
+ [Crux Logo] +

The Formal System λδ (\lambda\delta)

Towards the unification of terms, types, environments and contexts

- [Separator]
- + [Separator]
+
@@ -40,21 +35,16 @@

Computer-checked formal - specifications [Butterfly]

+ specifications [Butterfly] Resource - 1 below provides for the statically generated natural language + 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 + for the dynamically generated natural language representation of - λδ meta-theory (powered by the HELM + λδ meta-theory (powered by the HELM rendering engine).
Remarkably, λδ was born and developed in the digital format of resource 3 @@ -64,51 +54,42 @@ paper (as it happens for most currently digitalized Mathematics).
    -
  1. F. Guidi: lambdadelta +
  2. F. Guidi: lambdadelta (revised 2011-09). Formal - specification for Matita 0.5 + specification for Matita 0.5 (HTML pages generated by the HELM rendering engine)
    Here are the most relevant theorems proved in the formal specification:
    3. -
  3. F. Guidi: lambdadelta +
  4. F. Guidi: lambdadelta (revised 2011-09). Formal - specification for Matita 0.5 (HELM directory).
    + specification for Matita 0.5 (HELM directory).

    5. -
  5. F. Guidi: lambdadelta_1 +
  6. F. Guidi: lambdadelta_1 (revised 2011-09). Formal specification for Coq @@ -139,52 +114,34 @@ Formal proof scripts). BibTeX entry.
-

Tools [Butterfly]

- [Crux Logo] The λδ +

Tools [Butterfly]

+ [Crux Logo] The λδ Digital Library - (LDDL) is part of HELM + (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).
    + Jutting's specification in Automath).

- [Helena Logo] Helena + [Helena Logo] Helena is a λδ processor, implemented in Caml @@ -194,10 +151,8 @@ href="static/lddl/crg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.ht 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 + 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 @@ -215,19 +170,16 @@ href="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&path=%2Ftrunk% intermediate language. Features importation from ".hln" files containing λδ textual syntax. - The overall validation speed of the "Grundlagen + The overall validation speed of the "Grundlagen der Analysis" increases of 22% with respect to version 0.8.0. [Svn - revision: 11032] (archived + revision: 11032] (archived source code)
    -
  • Version 0.8.0 (2009-09). +
  • Version 0.8.0 (2009-09). Supports "basic_rg" λδ with naive implementation of impredicative sort inclusion. Features - importation from Automath + importation from Automath and exportation to XML. [Svn - revision: 10304] (archived + revision: 10304] (archived source code)
    • 2009-09. - Jutting's specification of Landau's "Grundlagen + Jutting's specification of Landau's "Grundlagen der Analysis" enters λδ Digital Library.
    • 2009-06. - Jutting's specification of Landau's "Grundlagen + Jutting's specification of Landau's "Grundlagen der Analysis" is - successfully processed, enabling sort inclusion.
      • + successfully processed, enabling sort inclusion.
-

Other resources [Butterfly]

+

Other resources [Butterfly]

  • A Jed mode for - editing ".hln" files (containing λδ textual syntax): helena.sl + editing ".hln" files (containing λδ textual syntax): helena.sl (revised 2010-11).
@@ -306,20 +241,12 @@ computer

- [Valid HTML 4.01 Transitional] [Use Any - Browser Here] [PNG Used Here]
+ [Valid HTML 4.01 Transitional] [Use Any + Browser Here] [PNG Used Here]

- Last update 2012-12-01 by Ferruccio + Last update 2012-12-01 by Ferruccio Guidi
- - + + \ No newline at end of file diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html index c27cbfb5a..a224e9df6 100644 --- a/helm/www/lambdadelta/index.html +++ b/helm/www/lambdadelta/index.html @@ -1,26 +1,20 @@ - - - - lambdadelta home page + + + + λδ home page + - - - - + +

-[Crux Logo] -

The Formal System λδ (lambdadelta)
+[Crux Logo] +

The Formal System λδ (\lambda\delta)

Towards the unification of terms, types, environments and contexts

-[Separator]
- +[Separator]
+
@@ -39,11 +33,9 @@ -

Foreword [Butterfly]

+

Foreword [Butterfly]

The formal system λδ -(lambdadelta) is a typed lambda calculus that pursues the static and +(\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.
@@ -75,64 +67,48 @@ expected to have the expressive power of λ→.
λδ comes in several versions listed in the following table, which includes the major milestones:

- +
- - - - - - - - - - - - - - - @@ -144,8 +120,7 @@ for the Internet Explorer -user [Butterfly] +user [Butterfly] To view this site correctly, please select a font with Unicode support. @@ -160,20 +135,10 @@ Options" entry → "General" tab → "Fonts" button.
Version
+ 		Version
Name
+ 		Name
Started
+ 		Started
Released
+ 		Released
Dismissed
+ 		Dismissed
2
+ 		2
basic_2
+ 		basic_2
April + April 2011
planned + planned in 2013
not + not planned yet
1
+ 		1
basic_1
+ 		basic_1
May + May 2004
November + November 2006
May + May 2008

-[Valid HTML 4.01 Transitional] [Use Any Browser Here] [PNG Used Here]
+[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 diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index 8bc12e324..8ca8c771d 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -1,25 +1,19 @@ - - - - lambdadelta home page + + + + λδ home page + - - - - + +

-[Crux Logo] -

The Formal System λδ (lambdadelta)
+[Crux Logo] +

The Formal System λδ (\lambda\delta)

Towards the unification of terms, types, environments and contexts

-[Separator]
- +[Separator]
+
@@ -237,23 +220,13 @@ this site as the first result.
@@ -38,12 +32,21 @@ -

News [Butterfly]

+

News [Butterfly]

+
    + +
  • December 2012. The character "_" is removed from the denomination "lambda_delta".
    +
    • +
      +
    • The denomination "\lambda\delta" is used in λδ-related texts.
      • +
    • The denomination "lambdadelta" is used in λδ-related identifiers.
      • +
    • Permanent λδ URL acquired: http://lambdadelta.info/ +(pointing at this site).
      • +
    +
  • September 2011. The -denomination "lambdadelta" changes to "lambdadelta". +denomination "lambda-delta" changes to "lambda_delta".
    • The character "-" is reserved in λδ textual syntax (recognized by Helena 0.8.1). @@ -52,17 +55,16 @@ denomination "lambdadelta" changes to "lambdadelta". 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://lambdadelta.info on -December 2012.
      -
      • +
    • + +
+ -

Visibility [Butterfly]

+

Visibility [Butterfly]

    -
  • February 2012. The Google search for formal system lambda delta gives +
  • 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 +
  • 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]
+[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