Tools

Tools $\lambda\delta butterfly$

Î»Î´ Digital Library (LDDL)

+ Open Symbolic Notation

- The Î»Î´ Digital Library is part of HELM - and contains resources expressed in the systems of the Î»Î´ family. + 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.

- Contents: - Landau's "Grundlagen der Analysis" - (from Jutting's specification in Automath). -

- Access: - static pages (updated 2015-01), - data set (updated 2014-12), - HELM server URL (updated 2014-12). -

- Examples: - - Grundlagen's definition "t234" - in Î»Î´ version 4. -

Helena

@@ -161,7 +143,7 @@ +3% with optimized compilation, +5% without optimized compilation. [Svn revision: 13108] (archived source code).

+
2015-06. The corrected specification of Landau's "Grundlagen der Analysis" is successfully validated in a Î»Prolog implementation of Î»Î´ version 3. @@ -182,29 +164,29 @@ Documentation (J3a). [Svn revision: 13035] (archived source code).
- +
- The specification of Landau's "Grundlagen der Analysis" for Coq 8: grundlagen_2.v (revised 2015-02).
- +
- The specification of Landau's "Grundlagen der Analysis" for Matita 0.99.2: grundlagen_2.tar.bz2 (revised 2015-02).
- +
- The corrected specification of Landau's "Grundlagen der Analysis": grundlagen_2.aut (revised 2014-12).
- +
- 2015-02. The translated specification of Landau's "Grundlagen der Analysis" is successfully validated in CC by Coq 8.4.3.
- +
- 2014-12. The corrected specification of Landau's "Grundlagen der Analysis" is successfully validated in Î»Î´ version 3. @@ -221,13 +203,13 @@ increases of 22% with respect to version 0.8.0. [Svn revision: 11032] (archived source code).
  - +
  - A Jed mode for editing ".hln" files (containing Î»Î´ textual syntax): helena.sl (revised 2010-11).
  - +
  - 2009-12. Helena appears in F. Wiedijk's @@ -245,19 +227,19 @@ Documentation (R2a). [Svn revision: 10304] (archived source code).
    - +
    - A Jed mode for editing ".aut" files (containing Automath textual syntax): automath.sl (revised 2008-07).
    - +
    - 2009-09. Jutting's specification of Landau's "Grundlagen der Analysis" enters Î»Î´ Digital Library.
    - +
    - 2009-06. Jutting's specification of Landau's "Grundlagen der Analysis" is successfully processed, enabling sort inclusion. @@ -265,8 +247,37 @@
  +
  + $[\lambda\delta digital library logo]$ Î»Î´ Digital Library (LDDL)
  +
  + The Î»Î´ Digital Library is part of HELM + and contains resources expressed in the systems of the Î»Î´ family. +
  +
  - + Contents: + Landau's "Grundlagen der Analysis" + (from Jutting's specification in Automath). +
  +
  - + Access: + static pages (updated 2015-01), + data set (updated 2014-12), + HELM server URL (updated 2014-12). +
  +
  - + Examples: + + Grundlagen's definition "t234" + in Î»Î´ version 4. +
  - + $\lambda\delta rainbow rule$
  
  @@ -291,6 +302,6 @@
  
  -
  Last update: Sat, 23 Jan 2016 00:45:18 +0100
  +
  Last update: Sun, 16 Apr 2017 15:42:49 +0200