The Svn revisions containing the stable versions of Helena are indicated next.
</body>
<topitem name="v2">
- <notice class="gamma" notice="Version 0.8.2 (2014-12)."/>
+ <notice class="gamma" notice="Version 0.8.2 (2015-02)."/>
Uses λδ "Version 3" with layer variables as core language.
- Supports exportation to Grafite
+ Supports exportation to Gallina
+ (the specification language of <link to="http://coq.inria.fr/">Coq</link>),
+ and to Grafite
(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.
- [Svn revision: 13005] (<rlink to="download/helena_0.8.2.tar.gz">archived source code</rlink>)
+ <rlink to="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"
+ for <link to="http://coq.inria.fr/">Coq 8</link>:
+ <rlink to="download/grundlagen_2.v">grundlagen_2.v</rlink>
+ (revised <notice class="gamma" notice="2015-02"/>).
+ </item><item>
The specification of Landau's "Grundlagen der Analysis"
for <link to="http://matita.cs.unibo.it/">Matita 0.99.2</link>:
<rlink to="download/grundlagen_2.tar.bz2">grundlagen_2.tar.bz2</rlink>
- (revised <notice class="gamma" notice="2014-12"/>).
+ (revised <notice class="gamma" notice="2015-02"/>).
</item><item>
The corrected specification of Landau's "Grundlagen der Analysis":
<rlink to="download/grundlagen_2.aut">grundlagen_2.aut</rlink>
(revised <notice class="gamma" notice="2014-12"/>).
+ </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>.
</item><item>
<notice class="gamma" notice="2014-12."/>
The corrected specification of Landau's "Grundlagen der Analysis"
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] (<rlink to="download/helena_0.8.1.tar.gz">archived source code</rlink>)
+ [Svn revision: 11032] (<rlink to="download/helena_0.8.1.tar.gz">archived source code</rlink>).
<list><item>
A <link to="http://www.jedsoft.org/jed/">Jed mode</link>
for editing ".hln" files (containing λδ textual syntax):
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#ldR4">Documentation (R4)</rlink>.
+ <rlink to="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>