From: Ferruccio Guidi Date: Fri, 9 Sep 2011 12:21:22 +0000 (+0000) Subject: - news update X-Git-Tag: make_still_working~2295 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cc57e6f6528ccc871a4d52d2ce4859c4a76fc0ca;p=helm.git - news update - the download directory is now complete --- diff --git a/helm/www/lambda_delta/documentation.html b/helm/www/lambda_delta/documentation.html index 657dfe229..71f208233 100644 --- a/helm/www/lambda_delta/documentation.html +++ b/helm/www/lambda_delta/documentation.html @@ -84,10 +84,11 @@ Guidi: + Landau's -"Grundlagen der Analysis" from Automath to lambda_delta ( (2009-09). University of Bologna, technical report UBLCS-2009-16. BibTeX entry.
@@ -153,7 +154,7 @@ entry.
1.2.
F. Guidi: Lambda Types on the Lambda Calculus with Abbreviations (2007-06). In @@ -169,6 +170,7 @@ In + CiE 2007 Local Proceedings. University of @@ -188,6 +190,7 @@ presentation). + BibTeX entry.

@@ -219,6 +222,7 @@ UBLCS-2006-25. + BibTeX entry.

@@ -262,7 +266,7 @@ System lambda-delta 1.6.
F. Guidi: Towards the Unification of Terms, Types and Contexts (2008-03). Presentation @@ -277,7 +281,7 @@ Types 1.7.
F. Guidi: Lambda Types on the Lambda Calculus with Abbreviations (2007-06). Presentation @@ -292,7 +296,7 @@ CiE 1.8.
F. Guidi: Lambda Tipi sul Lambda Calcolo con Abbreviazioni (2007-01). Presentation @@ -308,6 +312,7 @@ Padova + in Italian).

@@ -318,7 +323,7 @@ Italian).
F. Guidi: Lambda Tipi sul Lambda Calcolo con Abbreviazioni: una Specifica Certificata (2005-12). Presentation at @@ -340,13 +345,13 @@ Italian).
style="border: 0px solid ; width: 88px; height: 31px;"> [Use Any Browser Here] [PNG Used Here]

-Last update 2010-12-14 by Ferruccio +Last update 2011-09-09 by Ferruccio Guidi
diff --git a/helm/www/lambda_delta/download/PNGnow2.png b/helm/www/lambda_delta/download/PNGnow2.png new file mode 100644 index 000000000..dc25983fb Binary files /dev/null and b/helm/www/lambda_delta/download/PNGnow2.png differ diff --git a/helm/www/lambda_delta/download/cie_2007.pdf b/helm/www/lambda_delta/download/cie_2007.pdf new file mode 100644 index 000000000..d369a8bc3 Binary files /dev/null and b/helm/www/lambda_delta/download/cie_2007.pdf differ diff --git a/helm/www/lambda_delta/download/globe_trans.png b/helm/www/lambda_delta/download/globe_trans.png new file mode 100644 index 000000000..463b0be80 Binary files /dev/null and b/helm/www/lambda_delta/download/globe_trans.png differ diff --git a/helm/www/lambda_delta/download/lambda_delta_1.tar.gz b/helm/www/lambda_delta/download/lambda_delta_1.tar.gz new file mode 100644 index 000000000..d83966597 Binary files /dev/null and b/helm/www/lambda_delta/download/lambda_delta_1.tar.gz differ diff --git a/helm/www/lambda_delta/download/ld_talk_1s.pdf b/helm/www/lambda_delta/download/ld_talk_1s.pdf new file mode 100644 index 000000000..3f523b092 Binary files /dev/null and b/helm/www/lambda_delta/download/ld_talk_1s.pdf differ diff --git a/helm/www/lambda_delta/download/ld_talk_2s.pdf b/helm/www/lambda_delta/download/ld_talk_2s.pdf new file mode 100644 index 000000000..f7a3c9464 Binary files /dev/null and b/helm/www/lambda_delta/download/ld_talk_2s.pdf differ diff --git a/helm/www/lambda_delta/download/ld_talk_3s.pdf b/helm/www/lambda_delta/download/ld_talk_3s.pdf new file mode 100644 index 000000000..c3e18f6d6 Binary files /dev/null and b/helm/www/lambda_delta/download/ld_talk_3s.pdf differ diff --git a/helm/www/lambda_delta/download/ld_talk_4s.pdf b/helm/www/lambda_delta/download/ld_talk_4s.pdf new file mode 100644 index 000000000..6552c2140 Binary files /dev/null and b/helm/www/lambda_delta/download/ld_talk_4s.pdf differ diff --git a/helm/www/lambda_delta/implementation.html b/helm/www/lambda_delta/implementation.html index 27fbff71b..b7e1d0a8a 100644 --- a/helm/www/lambda_delta/implementation.html +++ b/helm/www/lambda_delta/implementation.html @@ -51,14 +51,14 @@ 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-TYPES -(revised 2008-06). Formal + style="font-style: italic;" href="static/matita/lambda_delta/">lambda_delta +(revised 2011-09). Formal specification with the proof assistant Matita 0.5 (HTML pages generated by the HELM @@ -66,15 +66,15 @@ rendering engine)
    Here are the most relevant theorems proved in the formal specification:
      -
    • March 2008. An -improvement of the -specification of λδ in Coq 7.3.1 begins: -
        +
      • March 2008. The +specification of λδ version 2 in Coq 7.3.1 begins: +
      • September 2007. @@ -197,15 +214,15 @@ Coq 7.3.1 begins.
        style="width: 37px; height: 37px;" alt="[Butterfly]" title="Butterfly" src="download/b4.png">
          -
        • November 2010. The Google +
        • November 2010. +The Google search formal system lambda delta gives 8 resources about λδ as the first results.
          -
        • November 2010. The Yahoo +
        • November 2010. +The Yahoo search formal system lambda delta gives 4 resources and 2 sub-resources about λδ as the first results.
        @@ -221,13 +238,13 @@ gives 4 resources and 2 sub-resources about λδ as the first results.
        • style="border: 0px solid ; width: 88px; height: 31px;"> [Use Any Browser Here] [PNG Used Here]
        + src="download/PNGnow2.png">

        -Last update 2010-12-14 by Ferruccio +Last update 2011-09-09 by Ferruccio Guidi