From: Ferruccio Guidi Date: Tue, 21 Feb 2012 10:37:41 +0000 (+0000) Subject: - site update X-Git-Tag: make_still_working~1946 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=77c6a180035cd63f3edd4db54bd7e9b411f9e85e;p=helm.git - site update --- diff --git a/helm/www/lambda_delta/documentation.html b/helm/www/lambda_delta/documentation.html index 71f208233..64120aa00 100644 --- a/helm/www/lambda_delta/documentation.html +++ b/helm/www/lambda_delta/documentation.html @@ -51,7 +51,7 @@ A summary of basic λδ (version below.

[Basic lambda_delta Logo] Basic λδ version 2:

+ src="download/basic_32.png"> Basic λδ version 2 (in progress): @@ -85,6 +85,7 @@ Guidi: + Landau's @@ -129,7 +130,7 @@ Bologna

[Basic lambda_delta Logo] Basic λδ version 1:

+ src="download/basic_32.png"> Basic λδ version 1 (closed): @@ -154,8 +155,8 @@ entry.
1.2.
 F. Guidi: Lambda Types on the Lambda Calculus with + href="download/cie_2007.pdf">Lambda +Types on the Lambda Calculus with Abbreviations (2007-06). In @@ -171,6 +172,7 @@ In + CiE 2007 Local Proceedings. University of @@ -191,6 +193,7 @@ presentation). + BibTeX entry.

@@ -223,6 +226,7 @@ UBLCS-2006-25. + BibTeX entry.

@@ -266,8 +270,8 @@ System lambda-delta 		1.6.
 F. Guidi: Towards the Unification of Terms, Types + href="download/ld_talk_4s.pdf">Towards +the Unification of Terms, Types and Contexts (2008-03). Presentation at @@ -281,8 +285,8 @@ Types 1.7.
 F. Guidi: Lambda Types on the Lambda Calculus with + href="download/ld_talk_3s.pdf">Lambda +Types on the Lambda Calculus with Abbreviations (2007-06). Presentation at @@ -296,8 +300,8 @@ CiE 1.8.
 F. Guidi: Lambda Tipi sul Lambda Calcolo con + href="download/ld_talk_2s.pdf">Lambda +Tipi sul Lambda Calcolo con Abbreviazioni (2007-01). Presentation at @@ -313,6 +317,7 @@ Padova + in Italian).

@@ -322,8 +327,7 @@ Italian).
1.9.
 F. -Guidi: Lambda Tipi sul Lambda Calcolo con Abbreviazioni: una Specifica Certificata (2005-12). Presentation at @@ -351,7 +355,7 @@ Italian).
title="PNG Used Here]" src="http://www.cs.unibo.it/%7Efguidi/download/PNGnow2.png">

-Last update 2011-09-09 by Ferruccio +Last update 2012-02-21 by Ferruccio Guidi
diff --git a/helm/www/lambda_delta/implementation.html b/helm/www/lambda_delta/implementation.html index 12458806e..79f013900 100644 --- a/helm/www/lambda_delta/implementation.html +++ b/helm/www/lambda_delta/implementation.html @@ -59,8 +59,8 @@ paper (as it happens for most currently digitalized Mathematics).
  • F. Guidi: lambda_delta (revised 2011-09). Formal -specification with the proof assistant Matita 0.5 (HTML pages generated +specification for Matita 0.5 +(HTML pages generated by the HELM rendering engine)
    Here are the most relevant theorems proved in the formal specification: @@ -110,17 +110,15 @@ problem.
    style="font-style: italic;" href="http://mowgli.cs.unibo.it:58080/apply?keys=RT&xmluri=http://helm.cs.unibo.it/helm//html/folder/index.html&prop.media-type=text/html&param.thmedia-type=text/html&param.thkeys=T1%2CT2%2CL%2CE&param.embedkeys=d_c%2CTC1%2CHC2%2CL&param.thencoding=UTF-8&prop.encoding=UTF-8&prop.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&param.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&param.encoding=UTF-8&param.media-type=text/html&param.keys=d_c%2CC1%2CHC2%2CL&profile=default&param.profile=default&param.CICURI=theory:/matita/lambda_delta/">lambda_delta (revised 2011-09). Formal -specification with the proof assistant Matita 0.5 (Matita 0.5 (HELM directory).

  • F. Guidi: lambda_delta_1 (revised 2011-09). -Formal specification with the proof assistant Coq 7.3.1 (source + href="download/lambda_delta_1.tar.gz">lambda_delta_1 +(revised 2011-09). +Formal specification for Coq 7.3.1 +(source proof scripts). BibTeX entry.
    • @@ -176,6 +174,13 @@ The processor source code is available in the directory 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. @@ -188,7 +193,8 @@ source code)
      • @@ -227,6 +233,7 @@ BibTeX database of λδ documentation: lambda_delta.bib, + lambda_delta.txt (revised 2011-09). @@ -265,10 +272,9 @@ editing ".aut" files (containing [PNG Used Here]
      + title="PNG Used Here" src="download/PNGnow2.png">

      -Last update 2011-09-09 by Ferruccio +Last update 2012-02-21 by Ferruccio Guidi
      diff --git a/helm/www/lambda_delta/news.html b/helm/www/lambda_delta/news.html index e3d13c5ee..a1c4024ec 100644 --- a/helm/www/lambda_delta/news.html +++ b/helm/www/lambda_delta/news.html @@ -54,7 +54,8 @@ 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.
      + style="font-style: italic;">http://lambda_delta.info on +December 2012.
    @@ -88,9 +89,10 @@ started.
    @@ -116,20 +119,21 @@ for publication.
    • March 2008. The -specification of λδ version 2 begins in Coq 7.3.1 (false start). +specification of λδ version 2 is started with Coq 7.3.1 (false start).