X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fweb%2Fhome%2Fimplementation.ldw.xml;h=9112a8037985ab0da12e3dc852c616d779995338;hb=e36a0eced135e6f1b79d06c78a408918f65376b6;hp=8e27e166b780f17a4fa1ee1e755f05b190012a05;hpb=68b5af5ca8f1e7f98485b92692b3dcb1ae240d19;p=helm.git diff --git a/helm/www/lambdadelta/web/home/implementation.ldw.xml b/helm/www/lambdadelta/web/home/implementation.ldw.xml index 8e27e166b..9112a8037 100644 --- a/helm/www/lambdadelta/web/home/implementation.ldw.xml +++ b/helm/www/lambdadelta/web/home/implementation.ldw.xml @@ -21,23 +21,20 @@ - static pages (updated ), - data set (updated ), - HELM server URL (updated ). + static pages (updated ), + data set (updated ), + HELM server URL (updated ). - + Grundlagen's definition "t234" - (in "basic_rg" λδ), - - Grundlagen's definition "t234" - (in "complete_rg" λδ). + in λδ version 4. Helena - Helena is a λδ processor, + Helena is a processor for λδ, 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. @@ -49,9 +46,35 @@ The Svn revisions containing the stable versions of Helena are indicated next. - - In progress. + + Uses λδ "Version 3" with layer variables as core language. + Supports exportation to Gallina + (the specification language of Coq), + and to Grafite + (the specification language of Matita). + The overall validation speed of the "Grundlagen der Analysis" + increases of 34% with respect to version 0.8.1. + Documentation (J4). + [Svn revision: 13035] (archived source code). + The specification of Landau's "Grundlagen der Analysis" + for Coq 8: + grundlagen_2.v + (revised ). + + The specification of Landau's "Grundlagen der Analysis" + for Matita 0.99.2: + grundlagen_2.tar.bz2 + (revised ). + + The corrected specification of Landau's "Grundlagen der Analysis": + grundlagen_2.aut + (revised ). + + + The translated specification of Landau's "Grundlagen der Analysis" + is successfully validated in λC by Coq 8.4.3. + The corrected specification of Landau's "Grundlagen der Analysis" is successfully validated in λδ "Version 3". @@ -59,11 +82,11 @@ - Uses a subset of λδ "Version 4" as the intermediate language. + Uses a subset of λδ "Version 4" as 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) + [Svn revision: 11032] (archived source code). A Jed mode for editing ".hln" files (containing λδ textual syntax):