X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fweb%2Fhome%2Fimplementation.ldw.xml;h=bd3f4e23bddfed69aca5d4499473a22f4057e8cb;hb=bc389dd4724959688aafc1ede450794f47b8d0b5;hp=05bb7c6c2cba7514f0db9c47ca2289f02a8c3728;hpb=c211eb61218aa9b43dfd2baae45407f0aa87ca79;p=helm.git diff --git a/helm/www/lambdadelta/web/home/implementation.ldw.xml b/helm/www/lambdadelta/web/home/implementation.ldw.xml index 05bb7c6c2..bd3f4e23b 100644 --- a/helm/www/lambdadelta/web/home/implementation.ldw.xml +++ b/helm/www/lambdadelta/web/home/implementation.ldw.xml @@ -3,7 +3,7 @@ @@ -12,7 +12,7 @@ λδ Digital Library (LDDL) The λδ Digital Library is part of HELM - and contains resources expressed in λδ. + and contains resources expressed in the systems of the λδ family. @@ -33,11 +33,12 @@ Helena + - Helena is a processor for λδ, + Helena is a processor for the systems of the λδ family, 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. + meant for testing both their stable and unstable features. The processor source code is available in the directory @@ -45,9 +46,29 @@ of the HELM Svn repository. The Svn revisions containing the stable versions of Helena are indicated next. + + + + Supports exportation to λProlog + (two formats for ELPI, + and two formats for Teyjus). + Employs optimized conditional compilation through + camlp5 code preprocessor (pa_macro) + to reduce a performance loss, which is expected to disappear + by employing a different code preprocessor. + Overall validation speed of the "Grundlagen der Analysis" with respect to version 0.8.2: + +3% with optimized compilation, +5% without optimized compilation. + [Svn revision: 13108] (archived source code). + + + The corrected specification of Landau's "Grundlagen der Analysis" + is successfully validated in a λProlog implementation of λδ version 3. + + + - Uses λδ "Version 3" with layer variables as core language. + Uses λδ version 3 with layer variables as core language. Supports exportation to Gallina (the specification language of Coq), and to Grafite @@ -73,16 +94,17 @@ The translated specification of Landau's "Grundlagen der Analysis" - is successfully validated in λC by Coq 8.4.3. + is successfully validated in CC by Coq 8.4.3. The corrected specification of Landau's "Grundlagen der Analysis" - is successfully validated in λδ "Version 3". + is successfully validated in λδ version 3. + - Uses a subset of λδ "Version 4" as 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. @@ -99,9 +121,10 @@ index of computer math systems. + - Supports λδ "Version 2" with naive implementation of impredicative sort inclusion. + Supports λδ version 2 with naive implementation of impredicative sort inclusion. Features importation from Automath and exportation to XML. Documentation (R2a). @@ -122,5 +145,6 @@ is successfully processed, enabling sort inclusion. +