<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.
<topitem name="source2">
<body>
- <rlink to="download/lambdadelta_2.tar.gz">lambdadelta_2 for Matita 0.99.2</rlink>
+ <rlink to="download/lambdadelta_2A1.tar.gz">lambdadelta_2A1 for Matita 0.99.2</rlink>
(revised <notice class="gamma" notice="2014-10"/>).
Source scripts.
+ <rlink to="documentation.html#ldR2c">Documentation (R2c)</rlink>.
</body>
<body>
The scripts are grouped in directories, first by part, then by component.
<rlink to="download/lambdadelta_1.tar.gz">lambdadelta_1 for Coq 7.3.1</rlink>
(revised <notice class="delta" notice="2015-09"/>).
Source scripts.
+ <rlink to="documentation.html#ldJ1a">Documentation (J1a)</rlink>.
<list><item>
<notice class="delta" notice="2015 January 15."/>
17 new lemmas and former lemma "eq_nat_dec" renamed as "nat_dec_neg".