X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fweb%2Fhome%2Fimplementation.ldw.xml;h=76bd89b33a94626779f64dd34c101189cb5099bd;hb=528f8ea107f689d07d060e1d31ba32bf65b4e6ba;hp=ef29ccc0fe81ce0832123538ee6d745b7f5907c9;hpb=3bd760474c12a1c527e24ac7ed39412d994e2db5;p=helm.git diff --git a/helm/www/lambdadelta/web/home/implementation.ldw.xml b/helm/www/lambdadelta/web/home/implementation.ldw.xml index ef29ccc0f..76bd89b33 100644 --- a/helm/www/lambdadelta/web/home/implementation.ldw.xml +++ b/helm/www/lambdadelta/web/home/implementation.ldw.xml @@ -3,41 +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 λδ version 4. - - Helena + + 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,16 +35,36 @@ 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 (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). + Documentation (J3a). [Svn revision: 13035] (archived source code). The specification of Landau's "Grundlagen der Analysis" @@ -77,12 +87,13 @@ 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,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 (R2a). + Documentation (R2a). [Svn revision: 10304] (archived source code). A Jed mode @@ -122,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). + + + + static pages (updated ), + data set (updated ), + HELM server URL (updated ). + + + + + Grundlagen's definition "t234" + in λδ version 4. + +