<page xmlns="http://lambdadelta.info/"
description = "\lambda\delta home page"
title = "\lambda\delta home page"
+ logo = "crux"
head = "The Formal Systems of the λδ (\lambda\delta) Family"
>
<sitemap name="sitemap"/>
<section5 name="tools">Tools</section5>
- <subsection name="lddl"><crux-icon/>λδ Digital Library (LDDL)</subsection>
+ <subsection name="osn"><img logo="osn"/>Open Symbolic Notation</subsection>
+
<body>
- The λδ Digital Library is part of <link to="http://helm.cs.unibo.it/">HELM</link>
- 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 <rlink to="osn/">OSN web site</rlink>.
</body>
- <topitem name="contents">
- <notice class="alpha" notice="Contents:"/>
- Landau's "Grundlagen der Analysis"
- (from Jutting's specification in <link to="http://www.win.tue.nl/automath/">Automath</link>).
- </topitem>
- <topitem name="access">
- <notice class="alpha" notice="Access:"/>
- <rlink to="static/lddl/">static pages</rlink> (updated <notice class="gamma" notice="2015-01"/>),
- <rlink to="download/lddl.tar.bz2">data set</rlink> (updated <notice class="gamma" notice="2014-12"/>),
- <rlink to="xml/">HELM server URL</rlink> (updated <notice class="gamma" notice="2014-12"/>).
- </topitem>
- <topitem name="examples">
- <notice class="alpha" notice="Examples:"/>
- <rlink to="static/lddl/Environment/grundlagen_2/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
- Grundlagen's definition "t234"</rlink>
- in λδ version 4.
- </topitem>
- <subsection name="helena"><helena-icon/>Helena</subsection>
+
+ <subsection name="helena"><img logo="helena"/>Helena</subsection>
<body>
Helena is a processor for the systems of the λδ family,
(the specification language of <link to="http://matita.cs.unibo.it/">Matita</link>).
The overall validation speed of the "Grundlagen der Analysis"
increases of 34% with respect to version 0.8.1.
- <rlink to="documentation.html#ldJ3a">Documentation (J3a)</rlink>.
+ <rlink to="html/documentation.html#ldJ3a">Documentation (J3a)</rlink>.
[Svn revision: 13035] (<rlink to="download/helena_0.8.2.tar.gz">archived source code</rlink>).
<list><item>
The specification of Landau's "Grundlagen der Analysis"
Supports λδ version 2 with naive implementation of impredicative sort inclusion.
Features importation from <link to="http://www.win.tue.nl/automath/">Automath</link>
and exportation to <link to="http://www.w3.org/XML/">XML</link>.
- <rlink to="documentation.html#ldR2a">Documentation (R2a)</rlink>.
+ <rlink to="html/documentation.html#ldR2a">Documentation (R2a)</rlink>.
[Svn revision: 10304] (<rlink to="download/helena_0.8.0.tar.gz">archived source code</rlink>).
<list><item>
A <link to="http://www.jedsoft.org/jed/">Jed mode</link>
</item></list>
</topitem>
- <subsection name="osn"><osn-icon/>Open Symbolic Notation</subsection>
- <body>
- Open Symbolic Notation (OSN) is an easy data-interchange textual format
- based on <link to="https://en.wikipedia.org/wiki/S-expression">symbolic expressions</link>.
- 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.
- </body>
+ <subsection name="lddl"><img logo="lddl"/>λδ Digital Library (LDDL)</subsection>
+
<body>
- An OSN text uses the <link to="http://www.utf-8.com/">UTF-8</link> character set
- and contains the next tokens:
+ The λδ Digital Library is part of <link to="http://helm.cs.unibo.it/">HELM</link>
+ and contains resources expressed in the systems of the λδ family.
</body>
- <list><item>
- <symbol> a non-empty sequence of the 66 characters + - . 0..9 A..Z _ a..z <newline/>
- this sequence can represents the identifiers and the numerical constants of most programming languages
- </item><item>
- <string> a sequence of characters wrapped with the delimiter " <newline/>
- every valid UTF-8 character whose code point is greater than U+001F is accepted eccept " \ <newline/>
- the next commonly accepted escape sequences are recognized: \0 \a \b \t \n \v \f \r \e \" \\ <newline/>
- morover, the escape sequences \x <two hexadecimal digits> and \u <four hexadecimal digits>
- allow to specify a character by its code point <newline/>
- finally the escape sequences \( for U+0002 and \) for U+0003 are available
- </item><item>
- <qualifier> the character :
- </item><item>
- <left> each of the characters ( < [ { <newline/>
- this token starts a compound symbolic expression
- </item><item>
- <right> each of the characters ) > ] } <newline/>
- this token ends a compound symbolic expression
- </item><item>
- <ignored> each of the characters U+0009..U+000D U+0020 , ; = <newline/>
- these characters are ignored and separate the other tokens
- </item><item>
- <reserved> any character not starting any other token <newline/>
- these characters are not allowed,
- and those in the range U+0021..U+007E are
- ! # $ % & ' * / ? @ \ ^ ` | ~
- </item></list>
+ <topitem name="contents">
+ <notice class="alpha" notice="Contents:"/>
+ Landau's "Grundlagen der Analysis"
+ (from Jutting's specification in <link to="http://www.win.tue.nl/automath/">Automath</link>).
+ </topitem>
+ <topitem name="access">
+ <notice class="alpha" notice="Access: "/>
+ <rlink to="html/lddl/">html pages</rlink> (updated <notice class="gamma" notice="2019-12"/>),
+ <rlink to="download/lddl.tar.bz2">data set</rlink> (updated <notice class="gamma" notice="2014-12"/>),
+ <rlink to="xml/">HELM server URL</rlink> (updated <notice class="gamma" notice="2014-12"/>).
+ </topitem>
+ <topitem name="examples">
+ <notice class="alpha" notice="Examples: "/>
+ <rlink to="html/lddl/Environment/grundlagen_2/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
+ Grundlagen's definition "t234"</rlink>
+ in λδ version 4.
+ </topitem>
<footer/>
</page>
projects / helm.git / blobdiff