]> matita.cs.unibo.it Git - helm.git/blob - helm/www/lambdadelta/web/home/implementation.ldw.xml
update in basic_2
[helm.git] / helm / www / lambdadelta / web / home / implementation.ldw.xml
1 <?xml version="1.0" encoding="UTF-8"?>
2
3 <page xmlns="http://lambdadelta.info/"
4       description = "\lambda\delta home page"
5       title = "\lambda\delta home page"
6       logo = "crux"
7       head = "The Formal Systems of the λδ (\lambda\delta) Family"
8 >
9    <sitemap name="sitemap"/>
10
11    <section5 name="tools">Tools</section5>
12
13    <subsection name="osn"><img logo="osn"/>Open Symbolic Notation</subsection>
14
15    <body>
16       Open Symbolic Notation, abbreviated OSN,
17       is an easy and flexible data-interchange text format
18       intended for the lightweight representation of
19       generic abstract syntax trees in the domain of formal languages.
20       Additional information is available at <rlink to="osn/">OSN web site</rlink>.
21    </body>
22
23
24    <subsection name="helena"><img logo="helena"/>Helena</subsection>
25
26    <body>
27       Helena is a processor for the systems of the λδ family,
28       implemented in <link to="http://caml.inria.fr/">Caml</link>
29       as a part of the <link to="http://helm.cs.unibo.it/">HELM</link> software,
30       meant for testing both their stable and unstable features.
31    </body>
32    <body>
33       The processor source code is available in the directory
34       <link to="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&amp;path=%2Ftrunk%2Fhelm%2Fsoftware%2Fhelena%2F&amp;rev=0&amp;sc=0">/trunk/helm/software/helena/</link>
35       of the <link to="http://helm.cs.unibo.it/software/index.html">HELM Svn repository</link>.
36       The Svn revisions containing the stable versions of Helena are indicated next.
37    </body>
38
39    <topitem name="v3">
40       <notice class="gamma" notice="Version 0.8.3 (2015-12)."/>
41       Supports exportation to λProlog
42       (two formats for ELPI,
43       and two formats for <link to="http://teyjus.cs.umn.edu/">Teyjus</link>).
44       Employs optimized conditional compilation through
45       <link to="http://camlp5.gforge.inria.fr/">camlp5</link> code preprocessor (pa_macro)
46       to reduce a performance loss, which is expected to disappear
47       by employing a different code preprocessor.
48       Overall validation speed of the "Grundlagen der Analysis" with respect to version 0.8.2:
49       +3% with optimized compilation, +5% without optimized compilation.
50       [Svn revision: 13108] (<rlink to="download/helena_0.8.3.tar.gz">archived source code</rlink>).
51       <list><item>
52          <notice class="gamma" notice="2015-06."/>
53          The corrected specification of Landau's "Grundlagen der Analysis"
54          is successfully validated in a λProlog implementation of λδ version 3.
55       </item></list>
56    </topitem>
57
58    <topitem name="v2">
59       <notice class="gamma" notice="Version 0.8.2 (2015-02)."/>
60       Uses λδ version 3 with layer variables as core language.
61       Supports exportation to Gallina
62       (the specification language of <link to="http://coq.inria.fr/">Coq</link>),
63       and to Grafite
64       (the specification language of <link to="http://matita.cs.unibo.it/">Matita</link>).
65       The overall validation speed of the "Grundlagen der Analysis"
66       increases of 34% with respect to version 0.8.1.
67       <rlink to="documentation.html#ldJ3a">Documentation (J3a)</rlink>.
68       [Svn revision: 13035] (<rlink to="download/helena_0.8.2.tar.gz">archived source code</rlink>).
69       <list><item>
70          The specification of Landau's "Grundlagen der Analysis"
71          for <link to="http://coq.inria.fr/">Coq 8</link>:
72          <rlink to="download/grundlagen_2.v">grundlagen_2.v</rlink>
73          (revised <notice class="gamma" notice="2015-02"/>).
74       </item><item>
75          The specification of Landau's "Grundlagen der Analysis"
76          for <link to="http://matita.cs.unibo.it/">Matita 0.99.2</link>:
77          <rlink to="download/grundlagen_2.tar.bz2">grundlagen_2.tar.bz2</rlink>
78          (revised <notice class="gamma" notice="2015-02"/>).
79       </item><item>
80          The corrected specification of Landau's "Grundlagen der Analysis":  
81          <rlink to="download/grundlagen_2.aut">grundlagen_2.aut</rlink>
82          (revised <notice class="gamma" notice="2014-12"/>).
83       </item><item>
84          <notice class="gamma" notice="2015-02."/>
85          The translated specification of Landau's "Grundlagen der Analysis"
86          is successfully validated in CC by <link to="http://coq.inria.fr/">Coq 8.4.3</link>.
87       </item><item>
88          <notice class="gamma" notice="2014-12."/>
89          The corrected specification of Landau's "Grundlagen der Analysis"
90          is successfully validated in λδ version 3.
91       </item></list>
92    </topitem>
93
94    <topitem name="v1">
95       <notice class="beta" notice="Version 0.8.1 (2010-11)."/>
96       Uses a subset of λδ version 4 as intermediate language.
97       Features importation from ".hln" files containing λδ textual syntax.
98       The overall validation speed of the "Grundlagen der Analysis"
99       increases of 22% with respect to version 0.8.0.
100       [Svn revision: 11032] (<rlink to="download/helena_0.8.1.tar.gz">archived source code</rlink>).
101       <list><item>
102          A <link to="http://www.jedsoft.org/jed/">Jed mode</link>
103          for editing ".hln" files (containing λδ textual syntax):
104          <rlink to="download/helena.sl">helena.sl</rlink>
105          (revised <notice class="alpha" notice="2010-11"/>).
106       </item><item>
107          <notice class="beta" notice="2009-12."/>
108          Helena appears in F. Wiedijk's
109          <link to="http://www.cs.ru.nl/%7Efreek/digimath/index.html#helena">
110             index of computer math systems</link>.
111       </item></list>
112    </topitem>
113
114    <topitem name="v0">
115       <notice class="beta" notice="Version 0.8.0 (2009-09)."/>
116       Supports λδ version 2 with naive implementation of impredicative sort inclusion.
117       Features importation from <link to="http://www.win.tue.nl/automath/">Automath</link>
118       and exportation to <link to="http://www.w3.org/XML/">XML</link>.
119       <rlink to="documentation.html#ldR2a">Documentation (R2a)</rlink>.
120       [Svn revision: 10304] (<rlink to="download/helena_0.8.0.tar.gz">archived source code</rlink>).
121       <list><item>
122          A <link to="http://www.jedsoft.org/jed/">Jed mode</link>
123          for editing ".aut" files
124          (containing <link to="http://www.win.tue.nl/automath/">Automath</link> textual syntax):
125          <rlink to="download/automath.sl">automath.sl</rlink>
126          (revised <notice class="gamma" notice="2008-07"/>).
127       </item><item>
128          <notice class="beta" notice="2009-09."/>
129          Jutting's specification of Landau's "Grundlagen der Analysis"
130          enters λδ Digital Library.
131       </item><item>
132          <notice class="beta" notice="2009-06."/>
133          Jutting's specification of Landau's "Grundlagen der Analysis"
134          is successfully processed, enabling sort inclusion.
135       </item></list>
136    </topitem>
137
138    <subsection name="lddl"><img logo="lddl"/>λδ Digital Library (LDDL)</subsection>
139
140    <body>
141       The λδ Digital Library is part of <link to="http://helm.cs.unibo.it/">HELM</link>
142       and contains resources expressed in the systems of the λδ family.      
143    </body>
144    <topitem name="contents">
145       <notice class="alpha" notice="Contents:"/>
146       Landau's "Grundlagen der Analysis"
147       (from Jutting's specification in  <link to="http://www.win.tue.nl/automath/">Automath</link>).
148    </topitem>
149    <topitem name="access">
150       <notice class="alpha" notice="Access:"/>
151       <rlink to="static/lddl/">static pages</rlink> (updated <notice class="gamma" notice="2015-01"/>),
152       <rlink to="download/lddl.tar.bz2">data set</rlink> (updated <notice class="gamma" notice="2014-12"/>),
153       <rlink to="xml/">HELM server URL</rlink> (updated <notice class="gamma" notice="2014-12"/>).
154    </topitem>
155    <topitem name="examples">
156       <notice class="alpha" notice="Examples:"/>
157       <rlink to="static/lddl/Environment/grundlagen_2/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
158          Grundlagen's definition "t234"</rlink>
159       in λδ version 4.
160    </topitem>
161
162    <footer/>
163 </page>