<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 10 Dec 2015 16:13:47 +0100</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 29 Dec 2015 22:50:57 +0100</div>
</body>
</html>
<img class="icon32" alt="[lambdadelta home]" title="lambdadelta home" src="http://lambdadelta.info/images/crux_32.png" />
</a>
</div>
- <div class="head1">The Formal System λδ (\lambda\delta)</div>
+ <div class="head1">The Formal Systems of the λδ (\lambda\delta) Family</div>
<div class="spacer">
<img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
</div>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 10 Dec 2015 16:13:46 +0100</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 12:08:04 +0100</div>
</body>
</html>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 10 Dec 2015 16:13:47 +0100</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 29 Dec 2015 22:50:57 +0100</div>
</body>
</html>
<img class="icon32" alt="[lambdadelta home]" title="lambdadelta home" src="http://lambdadelta.info/images/crux_32.png" />
</a>
</div>
- <div class="head1">The Formal System λδ (\lambda\delta)</div>
+ <div class="head1">The Formal Systems of the λδ (\lambda\delta) Family</div>
<div class="spacer">
<img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
</div>
<img class="icon32" alt="[Crux logo]" title="the Crux" src="http://lambdadelta.info/images/crux_32.png" /> λδ Digital Library (LDDL)</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
The λδ Digital Library is part of <a href="http://helm.cs.unibo.it/">HELM</a>
- and contains resources expressed in λδ.
+ and contains resources expressed in the systems of the λδ family.
</div>
<ul xmlns:ld="http://lambdadelta.info/" id="contents">
<li>
<div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="helena">
<img class="icon32" alt="[Helena logo]" title="Helena" src="http://lambdadelta.info/images/helena_32.png" /> Helena</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
- Helena is a processor for λδ,
+ Helena is a processor for the systems of the λδ family,
implemented in <a href="http://caml.inria.fr/">Caml</a>
as a part of the <a href="http://helm.cs.unibo.it/">HELM</a> 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.
</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
The processor source code is available in the directory
of the <a href="http://helm.cs.unibo.it/software/index.html">HELM Svn repository</a>.
The Svn revisions containing the stable versions of Helena are indicated next.
</div>
+ <ul xmlns:ld="http://lambdadelta.info/" id="v3">
+ <li>
+ <span class="emph gamma">Version 0.8.3 (2015-12).</span>
+ Supports exportation to λProlog
+ (two formats for ELPI,
+ and two formats for <a href="http://teyjus.cs.umn.edu/">Teyjus</a>).
+ Employs optimized conditional compilation through
+ <a href="http://camlp5.gforge.inria.fr/">camlp5</a> 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] (<a href="http://lambdadelta.info/download/helena_0.8.3.tar.gz">archived source code</a>).
+ <ul>
+ <li>
+ <span class="emph gamma">2015-06.</span>
+ The corrected specification of Landau's "Grundlagen der Analysis"
+ is successfully validated in a λProlog implementation of λδ version 3.
+ </li>
+ </ul>
+ </li>
+ </ul>
<ul xmlns:ld="http://lambdadelta.info/" id="v2">
<li>
<span class="emph gamma">Version 0.8.2 (2015-02).</span>
- 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 <a href="http://coq.inria.fr/">Coq</a>),
and to Grafite
<li>
<span class="emph gamma">2014-12.</span>
The corrected specification of Landau's "Grundlagen der Analysis"
- is successfully validated in λδ "Version 3".
+ is successfully validated in λδ version 3.
</li>
</ul>
</li>
<ul xmlns:ld="http://lambdadelta.info/" id="v1">
<li>
<span class="emph beta">Version 0.8.1 (2010-11).</span>
- 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.
<ul xmlns:ld="http://lambdadelta.info/" id="v0">
<li>
<span class="emph beta">Version 0.8.0 (2009-09).</span>
- Supports λδ "Version 2" with naive implementation of impredicative sort inclusion.
+ Supports λδ version 2 with naive implementation of impredicative sort inclusion.
Features importation from <a href="http://www.win.tue.nl/automath/">Automath</a>
and exportation to <a href="http://www.w3.org/XML/">XML</a>.
<a href="http://lambdadelta.info/documentation.html#ldR2a">Documentation (R2a)</a>.
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 10 Dec 2015 18:24:26 +0100</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 12:08:04 +0100</div>
</body>
</html>
<img class="icon32" alt="[lambdadelta home]" title="lambdadelta home" src="http://lambdadelta.info/images/crux_32.png" />
</a>
</div>
- <div class="head1">The Formal System λδ (\lambda\delta)</div>
+ <div class="head1">The Formal Systems of the λδ (\lambda\delta) Family</div>
<div class="spacer">
<img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
</div>
<div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="foreword">Foreword <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b9.png" />
</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
- The formal system λδ (\lambda\delta) is a typed λ-calculus aiming to support
+ The formal systems of the λδ (\lambda\delta) family are typed λ-calculi aiming to support
the foundational frameworks for Mathematics that require an underlying specification language
(for example the <a href="http://www.math.unipd.it/~maietti/">Minimalist Foundation</a>
and its predecessors).
</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
- λδ is developed in the context of the
+ The λδ family is developed within the
<a href="http://helm.cs.unibo.it/">Hypertextual Electronic Library of Mathematics</a>
- as a machine-checked digital specification
- that is not the formal counterpart of previous informal material.
+ as a set of machine-checked digital specifications.
</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
- This is the
System logo: <a href="http://lambdadelta.info/images/crux_177.png">crux_177.png</a>
+ This is the
family logo: <a href="http://lambdadelta.info/images/crux_177.png">crux_177.png</a>
(revised <span class="emph alpha">2012-09</span>).
</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
V. Rahili:
<span class="emph alpha">First Year Report: Realisability methods of proof and semantics with application to expansion</span>
(July 2007). Technical report.
+ </li>
+ </ul>
+ <!-- ===================================================================== -->
+ <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="disclaimer">Disclaimer <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b9.png" />
+ </div>
+ <div xmlns:ld="http://lambdadelta.info/" class="text">
+ The systens of the λδ family <span xmlns="http://lambdadelta.info/" class="emph">are not</span> related intentionally to any other system
+ having (variations of) the symbols λ and δ in its name or syntax.
+ Examples include (but are not limited to):
+ </div>
+ <ul xmlns:ld="http://lambdadelta.info/" id="D1">
+ <li>
+ <span xmlns="http://lambdadelta.info/" class="emph">λ-δ</span> of
+ A. Church:
+ <span xmlns="http://lambdadelta.info/" class="emph">The calculi of lambda-conversion</span>
+ (1941).
+ Annals of Mathematics Studies 6.
+ Princeton University Press.
+ </li>
+ </ul>
+ <ul xmlns:ld="http://lambdadelta.info/" id="D2">
+ <li>
+ <span xmlns="http://lambdadelta.info/" class="emph">∆Λ</span> of
+ N.G. de Bruijn:
+ <span xmlns="http://lambdadelta.info/" class="emph">Generalizing Automath by means of a lambda-typed lambda calculus</span>
+ (1987).
+ In Lecture Notes in Pure and Applied Mathematics 106, pp. 71-92.
+ Marcel Dekker.
+ </li>
+ </ul>
+ <ul xmlns:ld="http://lambdadelta.info/" id="D3">
+ <li>
+ <span xmlns="http://lambdadelta.info/" class="emph">λ<sub>∆</sub>
+ </span> of
+ N.J. Rehof, M.H. Sørensen:
+ <span xmlns="http://lambdadelta.info/" class="emph">The λ<sub>∆</sub>-calculus</span>
+ (1994).
+ In Lecture Notes in Computer Science, 789, pp. 516–542.
+ Springer.
+ </li>
+ </ul>
+ <ul xmlns:ld="http://lambdadelta.info/" id="D4">
+ <li>
+ <span xmlns="http://lambdadelta.info/" class="emph alpha">λ∆</span> of
+ S. Ronchi Della Rocca, L. Paolini:
+ <span xmlns="http://lambdadelta.info/" class="emph">The Parametric Lambda Calculus</span>
+ (2004).
+ Texts in Theoretical Computer Science, An EATCS Series.
+ Springer.
+ </li>
+ </ul>
+ <ul xmlns:ld="http://lambdadelta.info/" id="D5">
+ <li>
+ <span xmlns="http://lambdadelta.info/" class="emph">λD</span> of
+ R. Nederpelt, H. Geuvers:
+ <span xmlns="http://lambdadelta.info/" class="emph">Type Theory and Formal Proof</span>
+ (2014).
+ Cambridge University Press.
+ </li>
+ </ul>
+ <ul xmlns:ld="http://lambdadelta.info/" id="D6">
+ <li>
+ <span xmlns="http://lambdadelta.info/" class="emph">Cλξ</span> of
+ N.G. de Bruijn:
+ <span xmlns="http://lambdadelta.info/" class="emph">A namefree lambda calculus with facilities for internal definition of expressions and segments</span>
+ (1978).
+ TH-report 78-WSK-03.
+ Eindhoven University of Technology, Eindhoven.
</li>
</ul>
<div class="spacer">
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 10 Dec 2015 16:13:46 +0100</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 12:08:04 +0100</div>
</body>
</html>
<img class="icon32" alt="[lambdadelta home]" title="lambdadelta home" src="http://lambdadelta.info/images/crux_32.png" />
</a>
</div>
- <div class="head1">The Formal System λδ (\lambda\delta)</div>
+ <div class="head1">The Formal Systems of the λδ (\lambda\delta) Family</div>
<div class="spacer">
<img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
</div>
<!-- ===================================================================== -->
<div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="milestones">Milestones <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b3.png" />
</div>
+ <ul xmlns:ld="http://lambdadelta.info/">
+ <li>
+ <span class="emph gamma">December 2015.</span>
+ <a href="http://lambdadelta.info/implementation.html#v3">"Helena 0.8.3"</a> is released.
+ </li>
+ </ul>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph delta">August 2015.</span>
The specification of λδ version 2A1 is concluded.
+ </li>
+ </ul>
+ <ul xmlns:ld="http://lambdadelta.info/">
+ <li>
+ <span class="emph gamma">June 2015.</span>
+ The corrected specification of Landau's "Grundlagen der Analysis"
+ is validated in a λProlog implementation of λδ version 3.
</li>
</ul>
<ul xmlns:ld="http://lambdadelta.info/">
<span class="emph alpha">June 2014.</span>
The <a href="http://www.google.com/">Google</a>
search for "formal system lambda delta" gives
- 5 resources about λδ in the first 6 results.
+ 5 resources about the λδ family in the first 6 results.
</li>
</ul>
<ul xmlns:ld="http://lambdadelta.info/">
<span class="emph alpha">June 2014.</span>
The <a href="http://www.yahoo.com/">Yahoo</a>
search for "formal system lambda delta" gives
- 4 resources about λδ in the first 5 results.
+ 4 resources about the λδ family in the first 5 results.
</li>
</ul>
<div class="spacer">
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 10 Dec 2015 18:24:26 +0100</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 12:08:03 +0100</div>
</body>
</html>
<img class="icon32" alt="[lambdadelta home]" title="lambdadelta home" src="http://lambdadelta.info/images/crux_32.png" />
</a>
</div>
- <div class="head1">The Formal System λδ (\lambda\delta)</div>
+ <div class="head1">The Formal Systems of the λδ (\lambda\delta) Family</div>
<div class="spacer">
<img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
</div>
<div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="specifications">Computer-checked formal specifications <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b15.png" />
</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
- λδ is developed as a machine-checked digital specification.
- It comes in several versions listed in the next table,
- which includes the major milestones.
+ The systems of the λδ family are developed as machine-checked digital specifications,
+ and are listed in the next table, which includes the major milestones.
</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
The life cycle of a specification consists of four periods.
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 10 Dec 2015 16:21:42 +0100</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 12:08:04 +0100</div>
</body>
</html>
<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"/>
<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="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>
+
<footer/>
</page>
<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"/>
<section9 name="foreword">Foreword</section9>
<body>
- The formal system λδ (\lambda\delta) is a typed λ-calculus aiming to support
+ The formal systems of the λδ (\lambda\delta) family are typed λ-calculi aiming to support
the foundational frameworks for Mathematics that require an underlying specification language
(for example the <link to="http://www.math.unipd.it/~maietti/">Minimalist Foundation</link>
and its predecessors).
</body>
<body>
- λδ is developed in the context of the
+ The λδ family is developed within the
<link to="http://helm.cs.unibo.it/">Hypertextual Electronic Library of Mathematics</link>
- as a machine-checked digital specification
- that is not the formal counterpart of previous informal material.
+ as a set of machine-checked digital specifications.
</body>
<body>
- This is the System logo: <rlink to="images/crux_177.png">crux_177.png</rlink>
+ This is the family logo: <rlink to="images/crux_177.png">crux_177.png</rlink>
(revised <notice class="alpha" notice="2012-09"/>).
</body>
<body>
(July 2007). Technical report.
</topitem>
+<!-- ===================================================================== -->
+
+ <section9 name="disclaimer">Disclaimer</section9>
+ <body>
+ The systens of the λδ family <span class="emph">are not</span> related intentionally to any other system
+ having (variations of) the symbols λ and δ in its name or syntax.
+ Examples include (but are not limited to):
+ </body>
+
+ <topitem name="D1">
+ <span class="emph">λ-δ</span> of
+ A. Church:
+ <span class="emph">The calculi of lambda-conversion</span>
+ (1941).
+ Annals of Mathematics Studies 6.
+ Princeton University Press.
+ </topitem>
+
+ <topitem name="D2">
+ <span class="emph">∆Λ</span> of
+ N.G. de Bruijn:
+ <span class="emph">Generalizing Automath by means of a lambda-typed lambda calculus</span>
+ (1987).
+ In Lecture Notes in Pure and Applied Mathematics 106, pp. 71-92.
+ Marcel Dekker.
+ </topitem>
+
+ <topitem name="D3">
+ <span class="emph">λ<sub>∆</sub></span> of
+ N.J. Rehof, M.H. Sørensen:
+ <span class="emph">The λ<sub>∆</sub>-calculus</span>
+ (1994).
+ In Lecture Notes in Computer Science, 789, pp. 516–542.
+ Springer.
+ </topitem>
+
+ <topitem name="D4">
+ <span class="emph alpha">λ∆</span> of
+ S. Ronchi Della Rocca, L. Paolini:
+ <span class="emph">The Parametric Lambda Calculus</span>
+ (2004).
+ Texts in Theoretical Computer Science, An EATCS Series.
+ Springer.
+ </topitem>
+
+ <topitem name="D5">
+ <span class="emph">λD</span> of
+ R. Nederpelt, H. Geuvers:
+ <span class="emph">Type Theory and Formal Proof</span>
+ (2014).
+ Cambridge University Press.
+ </topitem>
+
+ <topitem name="D6">
+ <span class="emph">Cλξ</span> of
+ N.G. de Bruijn:
+ <span class="emph">A namefree lambda calculus with facilities for internal definition of expressions and segments</span>
+ (1978).
+ TH-report 78-WSK-03.
+ Eindhoven University of Technology, Eindhoven.
+ </topitem>
+
<footer/>
</page>
<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"/>
<section3 name="milestones">Milestones</section3>
+ <news class="gamma" date="December 2015.">
+ <rlink to="implementation.html#v3">"Helena 0.8.3"</rlink> is released.
+ </news>
+
<news class="delta" date="August 2015.">
The specification of λδ version 2A1 is concluded.
</news>
+ <news class="gamma" date="June 2015.">
+ The corrected specification of Landau's "Grundlagen der Analysis"
+ is validated in a λProlog implementation of λδ version 3.
+ </news>
+
<news class="delta" date="March 2015.">
The specification of λδ version 1 is validated by
<link to="http://matita.cs.unibo.it/">Matita 0.99.2</link>.
<news class="alpha" date="June 2014.">
The <link to="http://www.google.com/">Google</link>
search for "formal system lambda delta" gives
- 5 resources about λδ in the first 6 results.
+ 5 resources about the λδ family in the first 6 results.
</news>
<news class="alpha" date="June 2014.">
The <link to="http://www.yahoo.com/">Yahoo</link>
search for "formal system lambda delta" gives
- 4 resources about λδ in the first 5 results.
+ 4 resources about the λδ family in the first 5 results.
</news>
<footer/>
<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"/>
<section15 name="specifications">Computer-checked formal specifications</section15>
<body>
- λδ is developed as a machine-checked digital specification.
- It comes in several versions listed in the next table,
- which includes the major milestones.
+ The systems of the λδ family are developed as machine-checked digital specifications,
+ and are listed in the next table, which includes the major milestones.
</body>
<body>
The life cycle of a specification consists of four periods.
projects / helm.git / commitdiff