--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<page xmlns="http://lambdadelta.info/"
+ description = "\lambda\delta home page"
+ title = "\lambda\delta home page"
+ head = "The Formal System λδ (\lambda\delta)"
+>
+ <sitemap name="sitemap"/>
+
+ <section9 name="specifications">Computer-checked formal specifications</section9>
+ <body>
+ λδ comes in several versions listed in the following table,
+ which includes the major milestones:
+ </body>
+ <table name="versions"/>
+
+ <section5 name="tools">Tools</section5>
+
+ <section name="lddl"><crux-icon/>λδ Digital Library (LDDL)</section>
+ <body>
+ The λδ Digital Library is part of <link to="http://helm.cs.unibo.it/">HELM</link>
+ and contains resources expressed in λδ.
+ </body>
+ <news date="Contents:">
+ Landau's "Grundlagen der Analysis"
+ (from Jutting's specification in <link to="http://www.win.tue.nl/automath/">Automath</link>).
+ </news>
+ <news date="Access:">
+ <rlink to="static/lddl/">static pages</rlink> (updated <date date="2012-10"/>),
+ <rlink to="download/lddl.tar.bz2">data set</rlink> (updated <date date="2012-10"/>),
+ <rlink to="xml/">HELM server URL</rlink> (updated <date date="2012-10"/>).
+ </news>
+ <news date="Examples:">
+ <rlink to="static/lddl/brg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
+ Grundlagen's definition "t234"</rlink>
+ (in "basic_rg" λδ),
+ <rlink to="static/lddl/crg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
+ Grundlagen's definition "t234"</rlink>
+ (in "complete_rg" λδ).
+ </news>
+
+ <section name="helena"><helena-icon/>Helena</section>
+ <body>
+ Helena is a λδ processor,
+ 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.
+ </body>
+ <body>
+ The processor source code is available in the directory
+ <link to="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&path=%2Ftrunk%2Fhelm%2Fsoftware%2Fhelena%2F&rev=0&sc=0">/trunk/helm/software/helena/</link>
+ 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>
+ <news date="Version 0.8.2.">
+ In progress.
+ </news>
+ <news date="Version 0.8.1 (2010-11).">
+ Exploits a subset of "complete_rg" λδ as the intermediate language.
+ Features importation from ".hln" files containing λδ textual syntax.
+ The overall validation speed of the "Grundlagen der Analysis"
+ increases of 22% with respect toversion 0.8.0.
+ [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):
+ <rlink to="download/helena.sl">helena.sl</rlink>
+ (revised <date date="2010-11"/>).
+ </item><item>
+ <date date="2009-12."/>
+ Helena appears in F. Wiedijk's
+ <link to="http://www.cs.ru.nl/%7Efreek/digimath/index.html#helena">
+ index of computer math systems</link>.
+ </item></list>
+ </news>
+ <news date="Version 0.8.0 (2009-09).">
+ Supports "basic_rg" λδ 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#ldp6">Documentation</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>
+ for editing ".aut" files
+ (containing <link to="http://www.win.tue.nl/automath/">Automath</link> textual syntax):
+ <rlink to="download/automath.sl">automath.sl</rlink>
+ (revised <date date="2008-07"/>).
+ </item><item>
+ <date date="2009-09."/>
+ Jutting's specification of Landau's "Grundlagen der Analysis"
+ enters λδ Digital Library.
+ </item><item>
+ <date date="2009-06."/>
+ Jutting's specification of Landau's "Grundlagen der Analysis"
+ is successfully processed, enabling sort inclusion.
+ </item></list>
+ </news>
+ <footer/>
+</page>
projects / helm.git / blobdiff