X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fweb%2Fhome%2Fimplementation.ldw.xml;h=04ef6ed1a6fef2796885c0c7b11281610a63944b;hb=21e21b3b061807035bbd18d29d7a4fd8086ca10d;hp=fdc0ddba10924e2e8c45530507ccd45e2de3c9c5;hpb=9c489fe144c562dca776df59264329b704e18c49;p=helm.git diff --git a/helm/www/lambdadelta/web/home/implementation.ldw.xml b/helm/www/lambdadelta/web/home/implementation.ldw.xml index fdc0ddba1..04ef6ed1a 100644 --- a/helm/www/lambdadelta/web/home/implementation.ldw.xml +++ b/helm/www/lambdadelta/web/home/implementation.ldw.xml @@ -3,44 +3,31 @@ Tools - λδ Digital Library (LDDL) + Open Symbolic Notation + - The λδ Digital Library is part of HELM - and contains resources expressed in λδ. + Open Symbolic Notation, abbreviated OSN, + is an easy and flexible data-interchange text format + intended for the lightweight representation of + generic abstract syntax trees in the domain of formal languages. + Additional information is available at OSN web site. - - - Landau's "Grundlagen der Analysis" - (from Jutting's specification in Automath). - - - - static pages (updated ), - data set (updated ), - HELM server URL (updated ). - - - - - Grundlagen's definition "t234" - (in "basic_rg" λδ), - - Grundlagen's definition "t234" - (in "complete_rg" λδ). - - Helena + + Helena + - Helena is a λδ processor, + 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 @@ -48,31 +35,69 @@ 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. + + + - - 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 (J3a). + [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 ). + (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 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 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): @@ -85,12 +110,13 @@ 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 (R4). + Documentation (R2a). [Svn revision: 10304] (archived source code). A Jed mode @@ -108,5 +134,30 @@ is successfully processed, enabling sort inclusion. + + λδ Digital Library (LDDL) + + + The λδ Digital Library is part of HELM + and contains resources expressed in the systems of the λδ family. + + + + Landau's "Grundlagen der Analysis" + (from Jutting's specification in Automath). + + + + html pages (updated ), + data set (updated ), + HELM server URL (updated ). + + + + + Grundlagen's definition "t234" + in λδ version 4. + +