X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fweb%2Fhome%2Fimplementation.ldw.xml;h=229c5e88b45471517ff70ea0dcaf9f847e68fe34;hb=f7d7f2459b3b0409be5f168822be3b836ccc929b;hp=0613d899fb64e99f11c4950f1d2c5e052eb248e0;hpb=8ece314152135bef6cfc427482ee619a3c4fd0b8;p=helm.git diff --git a/helm/www/lambdadelta/web/home/implementation.ldw.xml b/helm/www/lambdadelta/web/home/implementation.ldw.xml index 0613d899f..229c5e88b 100644 --- a/helm/www/lambdadelta/web/home/implementation.ldw.xml +++ b/helm/www/lambdadelta/web/home/implementation.ldw.xml @@ -3,48 +3,42 @@ - Computer-checked formal specifications - - λδ comes in several versions listed in the following table, - which includes the major milestones: - - - Tools -
λδ Digital Library (LDDL)
+ λδ 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. - + + Landau's "Grundlagen der Analysis" (from Jutting's specification in Automath). - - - 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
- 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 @@ -52,48 +46,172 @@ of the HELM Svn repository. The Svn revisions containing the stable versions of Helena are indicated next. - - In progress. - - - Exploits a subset of "complete_rg" λδ as the intermediate language. + + + + 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. + 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 ). + + 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. + + + + + + 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): helena.sl - (revised ). + (revised ). - + Helena appears in F. Wiedijk's index of computer math systems. - - - Supports "basic_rg" λδ 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 for editing ".aut" files (containing Automath textual syntax): automath.sl - (revised ). + (revised ). - + Jutting's specification of Landau's "Grundlagen der Analysis" enters λδ Digital Library. - + Jutting's specification of Landau's "Grundlagen der Analysis" is successfully processed, enabling sort inclusion. - + + + Open Symbolic Notation + + Open Symbolic Notation (OSN) is an easy data-interchange textual format + based on symbolic expressions. + OSN is completely language independent but uses widely accepted conventions. + These features make OSN ideal for storing and exchanging tree-like data structures + in a lightweight manner. + + + An OSN text uses the UTF-8 character set + and contains the next tokens: + + + + + + + + + + + + + + this token can represent the identifiers and the numerical constants of most programming languages; + + + + + + + + + + every valid UTF-8 character whose code point is greater than U+001F is accepted eccept " \ + the next commonly accepted escape sequences are recognized: \0 \a \b \t \n \v \f \r \e \" \\ + morover, the escape sequences \x <two hexadecimal digits> and \u <four hexadecimal digits> + allow to specify a character by its code point + finally the escape sequences \( for U+0002 and \) for U+0003 are available + + + + + + + + + + + this token starts a compound symbolic expression; + + + + + + + this token ends a compound symbolic expression; + + <ignored> each of the characters U+0009..U+000D U+0020 , ; = + these characters are ignored and separate the other tokens + + <reserved> any character not starting any other token + these characters are not allowed, + and those in the range U+0021..U+007E are + ! # $ % & ' * / ? @ \ ^ ` | ~ + +