<page xmlns="http://lambdadelta.info/"
description = "\lambda\delta home page"
title = "\lambda\delta home page"
- head = "The Formal System λδ (\lambda\delta)"
+ head = "The Formal Systems of the λδ (\lambda\delta) Family"
>
<sitemap name="sitemap"/>
<subsection name="lddl"><crux-icon/>λδ Digital Library (LDDL)</subsection>
<body>
The λδ Digital Library is part of <link to="http://helm.cs.unibo.it/">HELM</link>
- and contains resources expressed in λδ.
+ and contains resources expressed in the systems of the λδ family.
</body>
<topitem name="contents">
<notice class="alpha" notice="Contents:"/>
</topitem>
<subsection name="helena"><helena-icon/>Helena</subsection>
+
<body>
- Helena is a processor for λδ,
+ Helena is a processor for the systems of the λδ family,
implemented in <link to="http://caml.inria.fr/">Caml</link>
as a part of the <link to="http://helm.cs.unibo.it/">HELM</link> 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.
</body>
<body>
The processor source code is available in the directory
of the <link to="http://helm.cs.unibo.it/software/index.html">HELM Svn repository</link>.
The Svn revisions containing the stable versions of Helena are indicated next.
</body>
+
+ <topitem name="v3">
+ <notice class="gamma" notice="Version 0.8.3 (2015-12)."/>
+ Supports exportation to λProlog
+ (two formats for ELPI,
+ and two formats for <link to="http://teyjus.cs.umn.edu/">Teyjus</link>).
+ Employs optimized conditional compilation through
+ <link to="http://camlp5.gforge.inria.fr/">camlp5</link> 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] (<rlink to="download/helena_0.8.3.tar.gz">archived source code</rlink>).
+ <list><item>
+ <notice class="gamma" notice="2015-06."/>
+ The corrected specification of Landau's "Grundlagen der Analysis"
+ is successfully validated in a λProlog implementation of λδ version 3.
+ </item></list>
+ </topitem>
+
<topitem name="v2">
<notice class="gamma" notice="Version 0.8.2 (2015-02)."/>
- 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 <link to="http://coq.inria.fr/">Coq</link>),
and to Grafite
</item><item>
<notice class="gamma" notice="2015-02."/>
The translated specification of Landau's "Grundlagen der Analysis"
- is successfully validated in λC by <link to="http://coq.inria.fr/">Coq 8.4.3</link>.
+ is successfully validated in CC by <link to="http://coq.inria.fr/">Coq 8.4.3</link>.
</item><item>
<notice class="gamma" notice="2014-12."/>
The corrected specification of Landau's "Grundlagen der Analysis"
- is successfully validated in λδ "Version 3".
+ is successfully validated in λδ version 3.
</item></list>
</topitem>
+
<topitem name="v1">
<notice class="beta" notice="Version 0.8.1 (2010-11)."/>
- 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.
index of computer math systems</link>.
</item></list>
</topitem>
+
<topitem name="v0">
<notice class="beta" notice="Version 0.8.0 (2009-09)."/>
- Supports λδ "Version 2" with naive implementation of impredicative sort inclusion.
+ 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>.
is successfully processed, enabling sort inclusion.
</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>
+ <body>
+ An OSN text uses the <link to="http://www.utf-8.com/">UTF-8</link> character set
+ and contains the next tokens:
+ </body>
+ <list><item>
+ <ebnf>
+ <prod of="symbol"/> <def/>
+ <prod of="symbol_char"/> <prod of="symbol_char"/> <star/>
+ <stop/> <newline/>
+ <prod of="symbol_char"/> <def/>
+ <chr of="+"/> <or/> <chr of="-"/> <or/> <chr of="."/> <or/>
+ <chr of="0"/> <or/> <etc/> <or/> <chr of="9"/> <or/>
+ <chr of="A"/> <or/> <etc/> <or/> <chr of="Z"/> <or/>
+ <chr of="_"/> <or/> <chr of="a"/> <or/> <etc/> <or/> <chr of="z"/>
+ <stop/>
+ </ebnf> <newline/>
+ this token can represent the identifiers and the numerical constants of most programming languages;
+ </item><item>
+ <ebnf>
+ <prod of="string"/> <def/>
+ <chr of="""/> <open/>
+ <prod of="string_char"/> <or/>
+ <chr of="\"/> <prod of="escape"/>
+ <close/> <star/> <chr of="""/>
+ <stop/>
+ </ebnf> <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>
+ <ebnf>
+ <prod of="qualifier"/> <def/> <chr of=":"/> <stop/>
+ </ebnf>
+ </item><item>
+ <ebnf>
+ <prod of="left"/> <def/>
+ <chr of="("/> <or/> <chr of="<"/> <or/> <chr of="["/> <or/> <chr of="{"/>
+ <stop/>
+ </ebnf> <newline/>
+ this token starts a compound symbolic expression;
+ </item><item>
+ <ebnf>
+ <prod of="right"/> <def/>
+ <chr of=")"/> <or/> <chr of=">"/> <or/> <chr of="]"/> <or/> <chr of="}"/>
+ <stop/>
+ </ebnf> <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>
+
<footer/>
</page>
projects / helm.git / blobdiff