<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 22 Oct 2014 20:00:29 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 28 Oct 2014 17:45:56 +0100</div>
</body>
</html>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
<meta http-equiv="Content-Style-Type" content="text/css" />
<meta name="author" content="Ferruccio Guidi" />
- <meta name="description" content="applications of \lambda\delta version 2" />
- <title>applications of \lambda\delta version 2</title>
+ <meta name="description" content="\lambda\delta home page" />
+ <title>\lambda\delta home page</title>
<link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/ld_web.css" />
<link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/lddl.css" />
<link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/xhtbl.css" />
<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="head2sn" id="">Contents of the Specification</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">
+ <br />
+ </div>
+ <div xmlns:ld="http://lambdadelta.info/" class="text">
+ <table cellpadding="4" cellspacing="0">
+ <tbody>
+ <tr>
+ <td class="snns capitalize italic sky">
+ <a href="http://lambdadelta.info/index.html">home</a>
+ </td>
+ <td class="snns capitalize italic magenta">
+ <a href="http://lambdadelta.info/news.html">news</a>
+ </td>
+ <td class="snns capitalize italic orange">
+ <a href="http://lambdadelta.info/documentation.html">documentation</a>
+ </td>
+ <td class="snns capitalize italic green">
+ <a href="http://lambdadelta.info/specification.html">specification</a>
+ </td>
+ <td class="snnn capitalize italic green">
+ <br />
+ </td>
+ <td class="ssns capitalize italic green">
+ <a href="http://lambdadelta.info/implementation.html">implementation</a>
+ </td>
+ </tr>
+ <tr>
+ <td class="snns capitalize sky">
+ <a href="http://lambdadelta.info/index.html#foreword">foreword</a>
+ </td>
+ <td class="snns capitalize magenta">
+ <a href="http://lambdadelta.info/news.html#milestones">milestones</a>
+ </td>
+ <td class="snns capitalize orange">
+ <a href="http://lambdadelta.info/documentation.html#v2">version 2</a>
+ </td>
+ <td class="snns capitalize green">
+ <a href="http://lambdadelta.info/specification.html#v2">version 2</a>
+ </td>
+ <td class="snnn capitalize green">(<a href="http://lambdadelta.info/ground_2.html">background</a> - <a href="http://lambdadelta.info/basic_2.html">core</a> - <a href="http://lambdadelta.info/apps_2.html">applications</a>)</td>
+ <td class="ssns capitalize green">
+ <a href="http://lambdadelta.info/implementation.html#lddl">library</a>
+ </td>
+ </tr>
+ <tr>
+ <td class="snss capitalize sky">
+ <a href="http://lambdadelta.info/index.html#citations">citations</a>
+ </td>
+ <td class="snss capitalize magenta">
+ <a href="http://lambdadelta.info/news.html#visibility">visibility</a>
+ </td>
+ <td class="snss capitalize orange">
+ <a href="http://lambdadelta.info/documentation.html#v1">version 1</a>
+ </td>
+ <td class="snss capitalize green">
+ <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
+ </td>
+ <td class="snsn capitalize green">
+ <br />
+ </td>
+ <td class="ssss capitalize green">
+ <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
+ </td>
+ </tr>
+ </tbody>
+ </table>
+ </div>
+
+ <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="contents">Contents of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
+ </div>
<div xmlns:ld="http://lambdadelta.info/" class="text">This specification comprises a collection of checked
applications of λδ version 2.
In particular it contains the components below.
</div>
- <ul xmlns:ld="http://lambdadelta.info/">
+ <ul xmlns:ld="http://lambdadelta.info/" id="MLTT1">
<li>
- <span class="date">MLTT1.</span>
- Martin-Löf's Type Theory with one universe
- using λδ as theory of expressions.
+ <span class="emph alpha">MLTT1.</span>
+ Martin-Löf's Type Theory with one universe
+ using λδ as theory of expressions.
</li>
</ul>
- <ul xmlns:ld="http://lambdadelta.info/">
+ <ul xmlns:ld="http://lambdadelta.info/" id="functional">
<li>
- <span class="date">Functional.</span>
- The validation algorithm for λδ as implemented in
-
<a href="http://lambdadelta.info/implementation.html#helena">Helena 0.8</a>.
+ <span class="emph alpha">Functional.</span>
+ The validation algorithm for λδ as implemented in
+ <a href="http://lambdadelta.info/implementation.html#helena">Helena 0.8</a>.
</li>
</ul>
- <div xmlns:ld="http://lambdadelta.info/" class="head2sn" id="">Summary of the Specification</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="summary">Summary of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
+ </div>
<div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical acount of the specification's contents
and its timeline.
- Nodes are counted according to the "intrinsinc complexity measure"
- [F. Guidi: "Procedural Representation of CIC Proof Terms"
- Journal of Automated Reasoning 44(1-2), Springer (February 2010),
- pp. 53-78].
</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
<table cellpadding="4" cellspacing="0">
</div>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">2012 February 24.</span>
+ <span class="emph alpha">2012 February 24.</span>
The Applications directory is started.
</li>
</ul>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">2011 December 20.</span>
+ <span class="emph alpha">2011 December 20.</span>
The Functional component is started
inside the specification of λδ version 2.
</li>
</ul>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">2011 December 12.</span>
+ <span class="emph alpha">2011 December 12.</span>
The MLTT1 component is started.
</li>
</ul>
- <div xmlns:ld="http://lambdadelta.info/" class="head2sn" id="">Logical Structure of the Specification</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">The source files are grouped in planes and components
- according to the following table.
- Each component contains its own notation file.
- The notation for the relations or functions introduced in each file
- is shown in parentheses (? are placeholders).
+ <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="structure">Logical Structure of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
+ </div>
+ <div xmlns:ld="http://lambdadelta.info/" class="text">This table reports the specification's components and their planes.
</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
<table cellpadding="4" cellspacing="0">
</table>
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="head2sn" id="">Physical Structure of the Specification</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">The source files are grouped in directories,
- one for each component.
- </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: Wed, 22 Oct 2014 20:00:29 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 28 Oct 2014 17:45:56 +0100</div>
</body>
</html>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
<meta http-equiv="Content-Style-Type" content="text/css" />
<meta name="author" content="Ferruccio Guidi" />
- <meta name="description" content="\lambda\delta version 2" />
- <title>\lambda\delta version 2</title>
+ <meta name="description" content="\lambda\delta home page" />
+ <title>\lambda\delta home page</title>
<link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/ld_web.css" />
<link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/lddl.css" />
<link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/xhtbl.css" />
<img class="icon32" alt="[lambdadelta home]" title="lambdadelta home" src="http://lambdadelta.info/images/crux_32.png" />
</a>
</div>
- <div class="head1">cic:/matita/lambdadelta/basic_2/ (λδ version 2)</div>
+ <div class="head1">cic:/matita/lambdadelta/basic_2/ (core λδ version 2)</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="text">
+ <table cellpadding="4" cellspacing="0">
+ <tbody>
+ <tr>
+ <td class="snns capitalize italic sky">
+ <a href="http://lambdadelta.info/index.html">home</a>
+ </td>
+ <td class="snns capitalize italic magenta">
+ <a href="http://lambdadelta.info/news.html">news</a>
+ </td>
+ <td class="snns capitalize italic orange">
+ <a href="http://lambdadelta.info/documentation.html">documentation</a>
+ </td>
+ <td class="snns capitalize italic green">
+ <a href="http://lambdadelta.info/specification.html">specification</a>
+ </td>
+ <td class="snnn capitalize italic green">
+ <br />
+ </td>
+ <td class="ssns capitalize italic green">
+ <a href="http://lambdadelta.info/implementation.html">implementation</a>
+ </td>
+ </tr>
+ <tr>
+ <td class="snns capitalize sky">
+ <a href="http://lambdadelta.info/index.html#foreword">foreword</a>
+ </td>
+ <td class="snns capitalize magenta">
+ <a href="http://lambdadelta.info/news.html#milestones">milestones</a>
+ </td>
+ <td class="snns capitalize orange">
+ <a href="http://lambdadelta.info/documentation.html#v2">version 2</a>
+ </td>
+ <td class="snns capitalize green">
+ <a href="http://lambdadelta.info/specification.html#v2">version 2</a>
+ </td>
+ <td class="snnn capitalize green">(<a href="http://lambdadelta.info/ground_2.html">background</a> - <a href="http://lambdadelta.info/basic_2.html">core</a> - <a href="http://lambdadelta.info/apps_2.html">applications</a>)</td>
+ <td class="ssns capitalize green">
+ <a href="http://lambdadelta.info/implementation.html#lddl">library</a>
+ </td>
+ </tr>
+ <tr>
+ <td class="snss capitalize sky">
+ <a href="http://lambdadelta.info/index.html#citations">citations</a>
+ </td>
+ <td class="snss capitalize magenta">
+ <a href="http://lambdadelta.info/news.html#visibility">visibility</a>
+ </td>
+ <td class="snss capitalize orange">
+ <a href="http://lambdadelta.info/documentation.html#v1">version 1</a>
+ </td>
+ <td class="snss capitalize green">
+ <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
+ </td>
+ <td class="snsn capitalize green">
+ <br />
+ </td>
+ <td class="ssss capitalize green">
+ <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
+ </td>
+ </tr>
+ </tbody>
+ </table>
+ </div>
- <div xmlns:ld="http://lambdadelta.info/" class="head2sn" id="">Summary of the Specification</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="summary">Summary of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
+ </div>
<div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical acount of the specification's contents
and its timeline.
- Nodes are counted according to the "intrinsinc complexity measure"
- [F. Guidi: "Procedural Representation of CIC Proof Terms"
- Journal of Automated Reasoning 44(1-2), Springer (February 2010),
- pp. 53-78].
</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
<table cellpadding="4" cellspacing="0">
<td class="snns italic cyan">files</td>
<td class="snnn right italic cyan">360</td>
<td class="snns italic cyan">characters</td>
- <td class="snnn right italic cyan">432823</td>
+ <td class="snnn right italic cyan">433402</td>
<td class="snns italic cyan">nodes</td>
- <td class="ssnn right italic cyan">1874185</td>
+ <td class="ssnn right italic cyan">1874774</td>
</tr>
<tr>
<td class="snns capitalize italic green">propositions</td>
<td class="snns italic green">theorems</td>
<td class="snnn right italic green">130</td>
<td class="snns italic green">lemmas</td>
- <td class="snnn right italic green">1288</td>
+ <td class="snnn right italic green">1286</td>
<td class="snns italic green">total</td>
- <td class="ssnn right italic green">1418</td>
+ <td class="ssnn right italic green">1416</td>
</tr>
<tr>
<td class="snss capitalize italic yellow">concepts</td>
</table>
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="">Stage "B"</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="B">Stage "B"</div>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">In progress.</span>
+ <span class="emph alpha">Ongoing.</span>
Context-sensitive subject equivalence
for native type assignment.
</li>
</ul>
- <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="">Stage "A": "Weakening the Applicability Condition"</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="A">Stage "A": "Extending the Applicability Condition"</div>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">2014 September 9.</span>
+ <span class="emph gamma">2014 October 28.</span>
+ λδ version 2A is released.
+ </li>
+ </ul>
+ <ul xmlns:ld="http://lambdadelta.info/">
+ <li>
+ <span class="emph beta">2014 September 9.</span>
Iterated static type assignment defined (more elegantly)
as a primitive notion.
</li>
</ul>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">2014 June 18.</span>
+ <span class="emph beta">2014 June 18.</span>
Preservation of stratified native validity
for context-sensitive computation on terms.
</li>
</ul>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">2014 June 9.</span>
+ <span class="emph alpha">2014 June 9.</span>
Strong qrst-normalization
for simply typed terms.
</li>
</ul>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">2014 April 16.</span>
+ <span class="emph alpha">2014 April 16.</span>
Lazy equivalence on local environments
addded as q-step to rst-computation on closures
(anniversary milestone).
</ul>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">2014 January 20.</span>
+ <span class="emph alpha">2014 January 20.</span>
Parametrized slicing of local environments
comprises both versions of this operation
(one from basic_1, the other used in basic_2 till now).
</ul>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">2013 August 7.</span>
+ <span class="emph alpha">2013 August 7.</span>
Passive support for global environments.
</li>
</ul>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">2013 July 27.</span>
+ <span class="emph alpha">2013 July 27.</span>
Reaxiomatized β-reductum as in rt-reduction.
</li>
</ul>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">2013 July 20.</span>
+ <span class="emph alpha">2013 July 20.</span>
Context-sensitive strong rt-normalization
for simply typed terms.
</li>
</ul>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">2013 April 16.</span>
+ <span class="emph alpha">2013 April 16.</span>
Reaxiomatized substitution and reduction
commute with respect to subclosure
(anniversary milestone).
</ul>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">2013 March 16.</span>
+ <span class="emph alpha">2013 March 16.</span>
Mutual recursive preservation of stratified native validity
for rst-computation on closures.
</li>
</ul>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">2012 October 16.</span>
+ <span class="emph alpha">2012 October 16.</span>
Confluence for context-free parallel reduction on closures.
</li>
</ul>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">2012 July 26.</span>
+ <span class="emph alpha">2012 July 26.</span>
Term binders polarized to control ζ-reduction (not released).
</li>
</ul>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">2012 April 16.</span>
+ <span class="emph alpha">2012 April 16.</span>
Context-sensitive subject equivalence
for atomic arity assignment
(anniversary milestone).
</ul>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">2012 March 15.</span>
+ <span class="emph alpha">2012 March 15.</span>
Context-sensitive strong normalization
for simply typed terms.
</li>
</ul>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">2012 January 27.</span>
+ <span class="emph alpha">2012 January 27.</span>
Support for abstract candidates of reducibility.
</li>
</ul>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">2011 September 21.</span>
+ <span class="emph alpha">2011 September 21.</span>
Confluence for context-sensitive parallel reduction on terms.
</li>
</ul>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">2011 September 6.</span>
+ <span class="emph alpha">2011 September 6.</span>
Confluence for context-free parallel reduction on terms.
</li>
</ul>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">2011 April 17.</span>
+ <span class="emph alpha">2011 April 17.</span>
Specification starts.
</li>
</ul>
- <div xmlns:ld="http://lambdadelta.info/" class="head2sn" id="">Logical Structure of the Specification</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">The source files are grouped in planes and components
- according to the following table.
- Notation files covering the whole specification are provided.
- The notation for the relations or functions introduced in each file
- is shown in parentheses (? are placeholders).
+ <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="structure">Logical Structure of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
+ </div>
+ <div xmlns:ld="http://lambdadelta.info/" class="text">This table reports the specification's components and their planes.
</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
<table cellpadding="4" cellspacing="0">
<br />
</td>
<td class="snns top cyan">cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )</td>
- <td class="snnn top cyan">cpxs_tsts cpxs_tsts_vector cpxs_leq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs</td>
+ <td class="snnn top cyan">cpxs_tsts cpxs_tsts_vector cpxs_lreq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs</td>
<td class="snnn top cyan">
<br />
</td>
<br />
</td>
<td class="snns top water">cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )</td>
- <td class="snnn top water">cpx_leq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix</td>
+ <td class="snnn top water">cpx_lreq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix</td>
<td class="snnn top water">
<br />
</td>
<br />
</td>
<td class="snns top yellow">lleq ( ? ≡[?,?] ? )</td>
- <td class="snnn top yellow">lleq_alt lleq_alt_rec lleq_leq lleq_drop lleq_fqus lleq_llor lleq_lleq</td>
+ <td class="snnn top yellow">lleq_alt lleq_alt_rec lleq_lreq lleq_drop lleq_fqus lleq_llor lleq_lleq</td>
<td class="snnn top yellow">
<br />
</td>
</td>
<td class="snns top italic yellow">lazy pointwise extension of a relation</td>
<td class="snns top yellow">llpx_sn</td>
- <td class="snnn top yellow">llpx_sn_alt llpx_sn_alt_rec llpx_sn_tc llpx_sn_leq llpx_sn_drop llpx_sn_lpx_sn llpx_sn_frees llpx_sn_llor</td>
+ <td class="snnn top yellow">llpx_sn_alt llpx_sn_alt_rec llpx_sn_tc llpx_sn_lreq llpx_sn_drop llpx_sn_lpx_sn llpx_sn_frees llpx_sn_llor</td>
<td class="snnn top yellow">
<br />
</td>
</td>
<td class="snns top italic yellow">context-sensitive exclusion from free variables</td>
<td class="snns top yellow">frees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )</td>
- <td class="snnn top yellow">frees_append frees_leq frees_lift</td>
+ <td class="snnn top yellow">frees_append frees_lreq frees_lift</td>
<td class="snnn top yellow">
<br />
</td>
</td>
<td class="snns top italic orange">basic local env. slicing</td>
<td class="snns top orange">drop ( ⬇[?,?,?] ? ≡ ? )</td>
- <td class="snnn top orange">drop_append drop_leq drop_drop</td>
+ <td class="snnn top orange">drop_append drop_lreq drop_drop</td>
<td class="snnn top orange">
<br />
</td>
<tr>
<td class="snns top capitalize italic red">grammar</td>
<td class="snns top italic red">equivalence for local environments</td>
- <td class="snns top red">leq ( ? ⩬[?,?] ? )</td>
- <td class="snnn top red">leq_leq</td>
+ <td class="snns top red">lreq ( ? ⩬[?,?] ? )</td>
+ <td class="snnn top red">lreq_lreq</td>
<td class="snnn top red">
<br />
</td>
</table>
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="head2sn" id="">Physical Structure of the Specification</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">The source files are grouped in directories,
- one for each component.
- </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: Wed, 22 Oct 2014 20:00:29 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 28 Oct 2014 17:45:56 +0100</div>
</body>
</html>
font-size: medium;
}
+span.emph {
+ font-weight: bold;
+ font-size: medium;
+}
+
span.date {
font-weight: bold;
font-size: medium;
height: 32px; /* this should be 31px */
}
+/* foreground colors (life cycle) *******************************************/
+
+.delta {
+ color:#500000;
+}
+
+.gamma {
+ color:#006000;
+}
+
+.beta {
+ color:#906000;
+}
+
+.alpha {
+ color:#000000;
+}
+
/* background colors ********************************************************/
.gray {
</tr>
<tr>
<td class="snss capitalize sky">
- <a href="http://lambdadelta.info/index.html#notice">notice</a>
+ <a href="http://lambdadelta.info/index.html#citations">citations</a>
</td>
<td class="snss capitalize magenta">
- <a href="http://lambdadelta.info/news.html#citations">citations</a>
+ <a href="http://lambdadelta.info/news.html#visibility">visibility</a>
</td>
<td class="snss capitalize orange">
<a href="http://lambdadelta.info/documentation.html#v1">version 1</a>
</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
BibTeX database of λδ documentation:
- <span class="date">download</span>
+ <span class="emph alpha">download</span>
<a href="http://lambdadelta.info/download/lambdadelta.bib">lambdadelta.bib</a>,
- <span class="date">view</span>
+ <span class="emph alpha">view</span>
<a href="http://lambdadelta.info/download/lambdadelta.txt">lambdadelta.txt</a>
- (revised <span class="date">2014-10</span>).
+ (revised <span class="emph gamma">2014-10</span>).
</div>
<div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="v2">
- <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" /> λδ version 2 (ongoing)</div>
+ <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" /> λδ version 2 (active)</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
- The main source of information is <span class="date">P8</span>.
+ The main source of information is <span class="emph alpha">P8</span>.
</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
<table cellpadding="4" cellspacing="0">
<tbody>
<tr>
<td class="snns top" id="ldR5">
- <span class="date">R5.</span>
+ <span class="emph alpha">R5.</span>
</td>
- <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/cie_2010.pdf">An Efficient Validation Procedure for the Formal System λδ</a> (<span class="
date">2010-07</span>). In CiE 2010 Local Proceedings. University of Azores, CMATI Booklet, pp. 204-213. <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
+ <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/cie_2010.pdf">An Efficient Validation Procedure for the Formal System λδ</a> (<span class="
emph alpha">2010-07</span>). In CiE 2010 Local Proceedings. University of Azores, CMATI Booklet, pp. 204-213. <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
</tr>
<tr>
<td class="nnns top" />
</tr>
<tr>
<td class="snns top" id="ldR4">
- <span class="date">R4.</span>
+ <span class="emph alpha">R4.</span>
</td>
- <td class="ssnn top">F. Guidi: <a href="http://www.informatica.unibo.it/it/ricerca/technical-report/2009/UBLCS-2009-16">Landau's "Grundlagen der Analysis" from Automath to lambda-delta</a> (<span class="
date">2009-09</span>). University of Bologna, technical report UBLCS-2009-16. <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
+ <td class="ssnn top">F. Guidi: <a href="http://www.informatica.unibo.it/it/ricerca/technical-report/2009/UBLCS-2009-16">Landau's "Grundlagen der Analysis" from Automath to lambda-delta</a> (<span class="
emph alpha">2009-09</span>). University of Bologna, technical report UBLCS-2009-16. <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
</tr>
<tr>
<td class="nnns top" />
</tr>
<tr>
<td class="snns top" id="ldP8">
- <span class="date">P8.</span>
+ <span class="emph alpha">P8.</span>
</td>
- <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_8s.pdf">The Formal System λδ and the "Three Problems"</a> (<span class="date">2014-06</span>). Presentation at University of Bologna (slides).</td>
+ <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_8s.pdf">The Formal System λδ and the "Three Problems"</a> (<span class="emph beta">2014-06</span>). Presentation at University of Bologna (slides).</td>
</tr>
<tr>
<td class="nnns top" />
</tr>
<tr>
<td class="snns top" id="ldP7">
- <span class="date">P7.</span>
+ <span class="emph alpha">P7.</span>
</td>
- <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_7s.pdf">An Efficient Validation Procedure for the Formal System λδ</a> (<span class="date">2010-07</span>). Presentation at CiE 2010 (slides).</td>
+ <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_7s.pdf">An Efficient Validation Procedure for the Formal System λδ</a> (<span class="emph alpha">2010-07</span>). Presentation at CiE 2010 (slides).</td>
</tr>
<tr>
<td class="nnns top" />
</tr>
<tr>
<td class="snns top" id="ldP6">
- <span class="date">P6.</span>
+ <span class="emph alpha">P6.</span>
</td>
- <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_6s.pdf">A Validator for the Formal System λδ</a> (revised <span class="date">2010-02</span>). Presentation at University of Bologna (slides).</td>
+ <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_6s.pdf">A Validator for the Formal System λδ</a> (revised <span class="emph alpha">2010-02</span>). Presentation at University of Bologna (slides).</td>
</tr>
<tr>
<td class="nnns top" />
</tr>
<tr>
<td class="snns top" id="ldV2">
- <span class="date">V2.</span>
+ <span class="emph alpha">V2.</span>
</td>
- <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/version_2.html">lambdadelta_2</a> (revised <span class="
date">2014-10</span>). Formal specification for the proof assistant Matita 0.99.2 (scripts). <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
+ <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/version_2.html">lambdadelta_2</a> (revised <span class="
emph gamma">2014-10</span>). Formal specification for the proof assistant Matita 0.99.2 (scripts). <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
</tr>
<tr>
<td class="nnss top" />
</div>
<div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="v1">
- <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b6.png" /> λδ version 1 (dismissed)</div>
+ <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b6.png" /> λδ version 1 (superseded)</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
- The main source of information is <span class="date">J1</span>.
- A summary is available in <span class="date">P5</span>.
+ The main source of information is <span class="emph alpha">J1</span>.
+ A summary is available in <span class="emph alpha">P5</span>.
</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
<table cellpadding="4" cellspacing="0">
<tbody>
<tr>
<td class="snns top" id="ldJ1">
- <span class="date">J1.</span>
+ <span class="emph alpha">J1.</span>
</td>
- <td class="ssnn top">F. Guidi: <a href="http://doi.acm.org/10.1145/1614431.1614436">The Formal System λδ</a> (<span class="
date">2009-11</span>). In ACM ToCL 11(1), pp. 5:1-5:37 (<a href="http://tocl.acm.org/accepted/335guidi.pdf">accepted</a>
- <span class="
date">2008-07</span>). CoRR identifier <a href="http://arxiv.org/abs/cs/0611040">cs/0611040</a> [v10] (revised <span class="date">2008-09</span>). <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
+ <td class="ssnn top">F. Guidi: <a href="http://doi.acm.org/10.1145/1614431.1614436">The Formal System λδ</a> (<span class="
emph delta">2009-11</span>). In ACM ToCL 11(1), pp. 5:1-5:37 (<a href="http://tocl.acm.org/accepted/335guidi.pdf">accepted</a>
+ <span class="
emph delta">2008-07</span>). CoRR identifier <a href="http://arxiv.org/abs/cs/0611040">cs/0611040</a> [v10] (revised <span class="emph delta">2008-09</span>). <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
</tr>
<tr>
<td class="nnns top" />
</tr>
<tr>
<td class="snns top" id="ldR3">
- <span class="date">R3.</span>
+ <span class="emph alpha">R3.</span>
</td>
- <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/cie_2007.pdf">Lambda Types on the Lambda Calculus with Abbreviations</a> (<span class="
date">2007-06</span>). In CiE 2007 Local Proceedings. University of Siena, technical report 487, p. 387 (abstract of a presentation). <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
+ <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/cie_2007.pdf">Lambda Types on the Lambda Calculus with Abbreviations</a> (<span class="
emph delta">2007-06</span>). In CiE 2007 Local Proceedings. University of Siena, technical report 487, p. 387 (abstract of a presentation). <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
</tr>
<tr>
<td class="nnns top" />
</tr>
<tr>
<td class="snns top" id="ldR2">
- <span class="date">R2.</span>
+ <span class="emph alpha">R2.</span>
</td>
- <td class="ssnn top">F. Guidi: <a href="http://www.informatica.unibo.it/it/ricerca/technical-report/2006/UBLCS-2006-25">Lambda Types on the Lambda Calculus with Abbreviations</a> (<span class="
date">2006-11</span>). University of Bologna, technical report UBLCS-2006-25. <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
+ <td class="ssnn top">F. Guidi: <a href="http://www.informatica.unibo.it/it/ricerca/technical-report/2006/UBLCS-2006-25">Lambda Types on the Lambda Calculus with Abbreviations</a> (<span class="
emph gamma">2006-11</span>). University of Bologna, technical report UBLCS-2006-25. <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
</tr>
<tr>
<td class="nnns top" />
</tr>
<tr>
<td class="snns top" id="ldR1">
- <span class="date">R1.</span>
+ <span class="emph alpha">R1.</span>
</td>
- <td class="ssnn top">F. Guidi: <a href="http://www.informatica.unibo.it/it/ricerca/technical-report/2006/UBLCS-2006-01">Lambda Types on the Lambda Calculus with Abbreviations: a Certified Specification</a> (<span class="
date">2006-01</span>). University of Bologna, technical report UBLCS-2006-01. <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
+ <td class="ssnn top">F. Guidi: <a href="http://www.informatica.unibo.it/it/ricerca/technical-report/2006/UBLCS-2006-01">Lambda Types on the Lambda Calculus with Abbreviations: a Certified Specification</a> (<span class="
emph beta">2006-01</span>). University of Bologna, technical report UBLCS-2006-01. <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
</tr>
<tr>
<td class="nnns top" />
</tr>
<tr>
<td class="snns top" id="ldP5">
- <span class="date">P5.</span>
+ <span class="emph alpha">P5.</span>
</td>
- <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_5s.pdf">The Formal System λδ</a> (<span class="date">2008-10</span>). Presentation at Advances in Constructive Topology and Logical Foundations (slides).</td>
+ <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_5s.pdf">The Formal System λδ</a> (<span class="emph delta">2008-10</span>). Presentation at Advances in Constructive Topology and Logical Foundations (slides).</td>
</tr>
<tr>
<td class="nnns top" />
</tr>
<tr>
<td class="snns top" id="ldP4">
- <span class="date">P4.</span>
+ <span class="emph alpha">P4.</span>
</td>
- <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_4s.pdf">Towards the Unification of Terms, Types and Contexts</a> (<span class="date">2008-03</span>). Presentation at Types 2008 (slides).</td>
+ <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_4s.pdf">Towards the Unification of Terms, Types and Contexts</a> (<span class="emph gamma">2008-03</span>). Presentation at Types 2008 (slides).</td>
</tr>
<tr>
<td class="nnns top" />
</tr>
<tr>
<td class="snns top" id="ldP3">
- <span class="date">P3.</span>
+ <span class="emph alpha">P3.</span>
</td>
- <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_3s.pdf">Lambda Types on the Lambda Calculus with Abbreviations</a> (<span class="date">2007-06</span>). Presentation at CiE 2007 (slides).</td>
+ <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_3s.pdf">Lambda Types on the Lambda Calculus with Abbreviations</a> (<span class="emph gamma">2007-06</span>). Presentation at CiE 2007 (slides).</td>
</tr>
<tr>
<td class="nnns top" />
</tr>
<tr>
<td class="snns top" id="ldP2">
- <span class="date">P2.</span>
+ <span class="emph alpha">P2.</span>
</td>
- <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_2s.pdf">Lambda Tipi sul Lambda Calcolo con Abbreviazioni</a> (<span class="date">2007-01</span>). Presentation at University of Padova (slides <span class="date">in Italian</span>).</td>
+ <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_2s.pdf">Lambda Tipi sul Lambda Calcolo con Abbreviazioni</a> (<span class="emph gamma">2007-01</span>). Presentation at University of Padova (slides <span class="emph alpha">in Italian</span>).</td>
</tr>
<tr>
<td class="nnns top" />
</tr>
<tr>
<td class="snns top" id="ldP1">
- <span class="date">P1.</span>
+ <span class="emph alpha">P1.</span>
</td>
- <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_1s.pdf">Lambda Tipi sul Lambda Calcolo con Abbreviazioni: una Specifica Certificata</a> (<span class="date">2005-12</span>). Presentation at University of Bologna (slides <span class="date">in Italian</span>).</td>
+ <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_1s.pdf">Lambda Tipi sul Lambda Calcolo con Abbreviazioni: una Specifica Certificata</a> (<span class="emph beta">2005-12</span>). Presentation at University of Bologna (slides <span class="emph alpha">in Italian</span>).</td>
</tr>
<tr>
<td class="nnns top" />
</tr>
<tr>
<td class="snns top" id="ldV1">
- <span class="date">V1.</span>
+ <span class="emph alpha">V1.</span>
</td>
- <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/version_1.html">lambdadelta_1</a> (revised <span class="
date">2012-10</span>). Formal specification for the proof assistant Coq 7.3.1 (scripts). <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
+ <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/version_1.html">lambdadelta_1</a> (revised <span class="
emph delta">2012-10</span>). Formal specification for the proof assistant Coq 7.3.1 (scripts). <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
</tr>
<tr>
<td class="nnss top" />
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 22 Oct 2014 20:00:28 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 28 Oct 2014 17:45:56 +0100</div>
</body>
</html>
-% \lambda\delta version 2 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% \lambda\delta version 2 (active) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@misc{lambdadeltaV2,
author="F. {Guidi}",
month="September"
}
-% \lambda\delta version 1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% \lambda\delta version 1 (superseded) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@article{lambdadeltaJ1,
author="F. {Guidi}",
-% \lambda\delta version 2 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% \lambda\delta version 2 (active) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@misc{lambdadeltaV2,
author="F. {Guidi}",
month="September"
}
-% \lambda\delta version 1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% \lambda\delta version 1 (superseded) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@article{lambdadeltaJ1,
author="F. {Guidi}",
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
<meta http-equiv="Content-Style-Type" content="text/css" />
<meta name="author" content="Ferruccio Guidi" />
- <meta name="description" content="background for \lambda\delta version 2" />
- <title>background for \lambda\delta version 2</title>
+ <meta name="description" content="\lambda\delta home page" />
+ <title>\lambda\delta home page</title>
<link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/ld_web.css" />
<link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/lddl.css" />
<link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/xhtbl.css" />
<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="head2sn" id="">Summary of the Specification</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">
+ <br />
+ </div>
+ <div xmlns:ld="http://lambdadelta.info/" class="text">
+ <table cellpadding="4" cellspacing="0">
+ <tbody>
+ <tr>
+ <td class="snns capitalize italic sky">
+ <a href="http://lambdadelta.info/index.html">home</a>
+ </td>
+ <td class="snns capitalize italic magenta">
+ <a href="http://lambdadelta.info/news.html">news</a>
+ </td>
+ <td class="snns capitalize italic orange">
+ <a href="http://lambdadelta.info/documentation.html">documentation</a>
+ </td>
+ <td class="snns capitalize italic green">
+ <a href="http://lambdadelta.info/specification.html">specification</a>
+ </td>
+ <td class="snnn capitalize italic green">
+ <br />
+ </td>
+ <td class="ssns capitalize italic green">
+ <a href="http://lambdadelta.info/implementation.html">implementation</a>
+ </td>
+ </tr>
+ <tr>
+ <td class="snns capitalize sky">
+ <a href="http://lambdadelta.info/index.html#foreword">foreword</a>
+ </td>
+ <td class="snns capitalize magenta">
+ <a href="http://lambdadelta.info/news.html#milestones">milestones</a>
+ </td>
+ <td class="snns capitalize orange">
+ <a href="http://lambdadelta.info/documentation.html#v2">version 2</a>
+ </td>
+ <td class="snns capitalize green">
+ <a href="http://lambdadelta.info/specification.html#v2">version 2</a>
+ </td>
+ <td class="snnn capitalize green">(<a href="http://lambdadelta.info/ground_2.html">background</a> - <a href="http://lambdadelta.info/basic_2.html">core</a> - <a href="http://lambdadelta.info/apps_2.html">applications</a>)</td>
+ <td class="ssns capitalize green">
+ <a href="http://lambdadelta.info/implementation.html#lddl">library</a>
+ </td>
+ </tr>
+ <tr>
+ <td class="snss capitalize sky">
+ <a href="http://lambdadelta.info/index.html#citations">citations</a>
+ </td>
+ <td class="snss capitalize magenta">
+ <a href="http://lambdadelta.info/news.html#visibility">visibility</a>
+ </td>
+ <td class="snss capitalize orange">
+ <a href="http://lambdadelta.info/documentation.html#v1">version 1</a>
+ </td>
+ <td class="snss capitalize green">
+ <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
+ </td>
+ <td class="snsn capitalize green">
+ <br />
+ </td>
+ <td class="ssss capitalize green">
+ <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
+ </td>
+ </tr>
+ </tbody>
+ </table>
+ </div>
+
+ <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="summary">Summary of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
+ </div>
<div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical acount of the specification's contents
and its timeline.
- Nodes are counted according to the "intrinsinc complexity measure"
- [F. Guidi: "Procedural Representation of CIC Proof Terms"
- Journal of Automated Reasoning 44(1-2), Springer (February 2010),
- pp. 53-78].
</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
<table cellpadding="4" cellspacing="0">
</div>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">2013 November 27.</span>
+ <span class="emph alpha">2013 November 27.</span>
Natural numbers with infinity.
</li>
</ul>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">2011 August 10.</span>
+ <span class="emph alpha">2011 August 10.</span>
Specification starts.
</li>
</ul>
- <div xmlns:ld="http://lambdadelta.info/" class="head2sn" id="">Logical Structure of the Specification</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">The source files are grouped in planes
- according to the following table.
- Notation files covering the whole specification are provided.
- The notation for the relations or functions introduced in each file
- is shown in parentheses (? are placeholders).
+ <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="structure">Logical Structure of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
+ </div>
+ <div xmlns:ld="http://lambdadelta.info/" class="text">This table reports the specification's components and their planes.
</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
<table cellpadding="4" cellspacing="0">
<tbody>
<tr>
+ <td class="snns top capitalize italic gray">component</td>
<td class="snns top italic gray">plane</td>
<td class="snns top gray">files</td>
<td class="snnn top gray">
</td>
</tr>
<tr>
- <td class="snns top italic yellow">natural numbers with infinity</td>
+ <td class="snns top capitalize italic yellow">natural numbers with infinity</td>
+ <td class="snns top italic yellow" />
<td class="snns top yellow">ynat ( ∞ )</td>
<td class="snnn top yellow">ynat_pred ( ⫰? )</td>
<td class="snnn top yellow">ynat_succ ( ⫯? )</td>
- <td class="snnn top yellow">ynat_le ( ?≤? )</td>
- <td class="snnn top yellow">ynat_lt ( ?<? )</td>
+ <td class="snnn top yellow">ynat_le ( ? ≤ ? )</td>
+ <td class="snnn top yellow">ynat_lt ( ? < ? )</td>
<td class="snnn top yellow">ynat_minus ( ? - ? )</td>
<td class="snnn top yellow">ynat_plus ( ? + ? )</td>
<td class="snnn top yellow">ynat_max</td>
<td class="ssnn top yellow">ynat_min</td>
</tr>
<tr>
- <td class="snns top italic orange">extensions to the library</td>
- <td class="snns top orange">arith.ma ( ?^? )</td>
- <td class="snnn top orange">
- <br />
- </td>
- <td class="snnn top orange">
- <br />
- </td>
- <td class="snnn top orange">
- <br />
- </td>
- <td class="snnn top orange">
- <br />
- </td>
+ <td class="snns top capitalize italic orange">extensions to the library</td>
+ <td class="snns top italic orange" />
+ <td class="snns top orange">star</td>
+ <td class="snnn top orange">lstar</td>
+ <td class="snnn top orange">bool ( Ⓕ ) ( Ⓣ )</td>
+ <td class="snnn top orange">arith ( ?^? )</td>
+ <td class="snnn top orange">list ( ◊ ) ( ? @ ? ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )</td>
<td class="snnn top orange">
<br />
</td>
</td>
</tr>
<tr>
- <td class="snss top italic red">generated logical decomposables</td>
+ <td class="snss top capitalize italic red">generated logical decomposables</td>
+ <td class="snss top italic red" />
<td class="snss top red">xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )</td>
<td class="snsn top red">xoa_props ( ⊥ ) ( ⊤ )</td>
<td class="snsn top red">
</table>
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="head2sn" id="">Physical Structure of the Specification</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">The source files are grouped in directories,
- one for each plane.
- </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: Wed, 22 Oct 2014 20:00:29 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 28 Oct 2014 17:45:56 +0100</div>
</body>
</html>
</tr>
<tr>
<td class="snss capitalize sky">
- <a href="http://lambdadelta.info/index.html#notice">notice</a>
+ <a href="http://lambdadelta.info/index.html#citations">citations</a>
</td>
<td class="snss capitalize magenta">
- <a href="http://lambdadelta.info/news.html#citations">citations</a>
+ <a href="http://lambdadelta.info/news.html#visibility">visibility</a>
</td>
<td class="snss capitalize orange">
<a href="http://lambdadelta.info/documentation.html#v1">version 1</a>
The λδ Digital Library is part of <a href="http://helm.cs.unibo.it/">HELM</a>
and contains resources expressed in λδ.
</div>
- <ul xmlns:ld="http://lambdadelta.info/">
+ <ul xmlns:ld="http://lambdadelta.info/" id="contents">
<li>
- <span class="date">Contents:</span>
+ <span class="emph alpha">Contents:</span>
Landau's "Grundlagen der Analysis"
(from Jutting's specification in <a href="http://www.win.tue.nl/automath/">Automath</a>).
</li>
</ul>
- <ul xmlns:ld="http://lambdadelta.info/">
+ <ul xmlns:ld="http://lambdadelta.info/" id="access">
<li>
- <span class="date">Access:</span>
- <a href="http://lambdadelta.info/static/lddl/">static pages</a> (updated <span class="date">2012-10</span>),
- <a href="http://lambdadelta.info/download/lddl.tar.bz2">data set</a> (updated <span class="date">2012-10</span>),
- <a href="http://lambdadelta.info/xml/">HELM server URL</a> (updated <span class="date">2012-10</span>).
+ <span class="emph alpha">Access:</span>
+ <a href="http://lambdadelta.info/static/lddl/">static pages</a> (updated <span class="emph beta">2012-10</span>),
+ <a href="http://lambdadelta.info/download/lddl.tar.bz2">data set</a> (updated <span class="emph beta">2012-10</span>),
+ <a href="http://lambdadelta.info/xml/">HELM server URL</a> (updated <span class="emph beta">2012-10</span>).
</li>
</ul>
- <ul xmlns:ld="http://lambdadelta.info/">
+ <ul xmlns:ld="http://lambdadelta.info/" id="examples">
<li>
- <span class="date">Examples:</span>
+ <span class="emph alpha">Examples:</span>
<a href="http://lambdadelta.info/static/lddl/brg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
Grundlagen's definition "t234"</a>
(in "basic_rg" λδ),
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/">
+ <ul xmlns:ld="http://lambdadelta.info/" id="v2">
<li>
- <span class="date">Version 0.8.2.</span>
+ <span class="emph beta">Version 0.8.2.</span>
In progress.
</li>
</ul>
- <ul xmlns:ld="http://lambdadelta.info/">
+ <ul xmlns:ld="http://lambdadelta.info/" id="v1">
<li>
- <span class="date">Version 0.8.1 (2010-11).</span>
+ <span class="emph beta">Version 0.8.1 (2010-11).</span>
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"
A <a href="http://www.jedsoft.org/jed/">Jed mode</a>
for editing ".hln" files (containing λδ textual syntax):
<a href="http://lambdadelta.info/download/helena.sl">helena.sl</a>
- (revised <span class="date">2010-11</span>).
+ (revised <span class="emph alpha">2010-11</span>).
</li>
<li>
- <span class="date">2009-12.</span>
+ <span class="emph beta">2009-12.</span>
Helena appears in F. Wiedijk's
<a href="http://www.cs.ru.nl/%7Efreek/digimath/index.html#helena">
index of computer math systems</a>.
</ul>
</li>
</ul>
- <ul xmlns:ld="http://lambdadelta.info/">
+ <ul xmlns:ld="http://lambdadelta.info/" id="v0">
<li>
- <span class="date">Version 0.8.0 (2009-09).</span>
+ <span class="emph beta">Version 0.8.0 (2009-09).</span>
Supports "basic_rg" λδ 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>.
for editing ".aut" files
(containing <a href="http://www.win.tue.nl/automath/">Automath</a> textual syntax):
<a href="http://lambdadelta.info/download/automath.sl">automath.sl</a>
- (revised <span class="date">2008-07</span>).
+ (revised <span class="emph gamma">2008-07</span>).
</li>
<li>
- <span class="date">2009-09.</span>
+ <span class="emph beta">2009-09.</span>
Jutting's specification of Landau's "Grundlagen der Analysis"
enters λδ Digital Library.
</li>
<li>
- <span class="date">2009-06.</span>
+ <span class="emph beta">2009-06.</span>
Jutting's specification of Landau's "Grundlagen der Analysis"
is successfully processed, enabling sort inclusion.
</li>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 22 Oct 2014 20:00:29 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 28 Oct 2014 17:45:56 +0100</div>
</body>
</html>
</tr>
<tr>
<td class="snss capitalize sky">
- <a href="http://lambdadelta.info/index.html#notice">notice</a>
+ <a href="http://lambdadelta.info/index.html#citations">citations</a>
</td>
<td class="snss capitalize magenta">
- <a href="http://lambdadelta.info/news.html#citations">citations</a>
+ <a href="http://lambdadelta.info/news.html#visibility">visibility</a>
</td>
<td class="snss capitalize orange">
<a href="http://lambdadelta.info/documentation.html#v1">version 1</a>
</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>
- (revised <span class="date">2012-09</span>).
+ (revised <span class="emph alpha">2012-09</span>).
</div>
-
- <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="notice">Notice for the Internet Explorer user <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b9.png" />
- </div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
+ <span class="emph alpha">Notice for the user of Internet Explorer.</span>
To view this site correctly, please select a font
with <a href="http://www.unicode.org/">Unicode</a> support.
For example "Lucida Sans Unicode" (it should be already installed on your system).
"Tools" menu → "Internet Options" entry → "General" tab → "Fonts" button.
</div>
+
+
+ <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="citations">Citations <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b9.png" />
+ </div>
+ <div xmlns:ld="http://lambdadelta.info/" class="text">
+ This is a list of publications citing λδ (not including our own).
+ </div>
+
+ <ul xmlns:ld="http://lambdadelta.info/" id="C6">
+ <li>
+ A. Asperti, W. Ricciotti, C. Sacerdoti Coen, E. Tassi:
+ <span class="emph alpha">Formal metatheory of programming languages in the Matita interactive theorem prover</span>
+ (2012). In JAR 49(3), pp. 427-451.
+ </li>
+ </ul>
+
+ <ul xmlns:ld="http://lambdadelta.info/" id="C5">
+ <li>
+ M.E. Maietti:
+ <span class="emph alpha">Consistency of the minimalist foundation with Church thesis and Bar Induction</span>
+ (2012). Submitted article.
+ </li>
+ </ul>
+
+ <ul xmlns:ld="http://lambdadelta.info/" id="C4">
+ <li>
+ W. Ricciotti:
+ <span class="emph alpha">Theoretical and implementation aspects in the mechanization of the metatheory of programming languages</span>
+ (July 2011). Ph.D. Thesis in Computer Science, Technical Report UBLCS-2011-09, University of Bologna.
+ </li>
+ </ul>
+
+ <ul xmlns:ld="http://lambdadelta.info/" id="C3">
+ <li>
+ C.E. Brown:
+ <span class="emph alpha">Faithful Reproductions of the Automath Landau Formalization</span>
+ (2011). Typescript note.
+ </li>
+ </ul>
+
+ <ul xmlns:ld="http://lambdadelta.info/" id="C2">
+ <li>
+ M.E. Maietti:
+ <span class="emph alpha">A minimalist two-level foundation for constructive mathematics</span>
+ (2009). In APAL 160(3), pp. 319-354.
+ </li>
+ </ul>
+
+ <ul xmlns:ld="http://lambdadelta.info/" id="C1">
+ <li>
+ V. Rahili:
+ <span class="emph alpha">First Year Report: Realisability methods of proof and semantics with application to expansion</span>
+ (July 2007). Typescript note.
+ </li>
+ </ul>
+
<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: Wed, 22 Oct 2014 20:00:29 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 28 Oct 2014 17:45:56 +0100</div>
</body>
</html>
</tr>
<tr>
<td class="snss capitalize sky">
- <a href="http://lambdadelta.info/index.html#notice">notice</a>
+ <a href="http://lambdadelta.info/index.html#citations">citations</a>
</td>
<td class="snss capitalize magenta">
- <a href="http://lambdadelta.info/news.html#citations">citations</a>
+ <a href="http://lambdadelta.info/news.html#visibility">visibility</a>
</td>
<td class="snss capitalize orange">
<a href="http://lambdadelta.info/documentation.html#v1">version 1</a>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">July 2014.</span>
+ <span class="emph beta">July 2014.</span>
A new version of this site is online.
</li>
</ul>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">June 2014.</span>
+ <span class="emph beta">June 2014.</span>
<a href="http://lambdadelta.info/documentation.html#ldP8">First communication on λδ version 2.</a>
</li>
</ul>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">December 2012.</span>
+ <span class="emph alpha">December 2012.</span>
The character "_" is removed from the denomination "lambda_delta":
<ul>
<li>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">September 2011.</span>
+ <span class="emph alpha">September 2011.</span>
The denomination "lambda-delta" changes to "lambda_delta":
<ul>
<li>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">April 2011.</span>
+ <span class="emph alpha">April 2011.</span>
The specification of <a href="http://lambdadelta.info/version_2.html">λδ version 2</a>
and related topics is restarted in
<a href="http://matita.cs.unibo.it/">Matita 0.5</a>.
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">December 2010.</span>
+ <span class="emph delta">February 2011.</span>
+ The specification of λδ version 2 with Coq 7.3.1 is abandoned.
+ </li>
+ </ul>
+
+ <ul xmlns:ld="http://lambdadelta.info/">
+ <li>
+ <span class="emph alpha">December 2010.</span>
Transient λδ URL acquired: http://lambda-delta.info/ (expires on December 2012).
</li>
</ul>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">November 2010.</span>
+ <span class="emph beta">November 2010.</span>
"Helena 0.8.1" is released.
</li>
</ul>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">September 2009.</span>
+ <span class="emph beta">September 2009.</span>
"Helena 0.8.0" is released and the
<a href="http://lambdadelta.info/implementation.html#lddl">λδ Digital Library</a>
is started.
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">June 2009.</span>
+ <span class="emph alpha">June 2009.</span>
"Helena", a <a href="http://lambdadelta.info/implementation.html#helena">validator for λδ version 2</a>,
is available as a part of the <a href="http://helm.cs.unibo.it/">HELM</a> software.
</li>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">September 2008.</span>
+ <span class="emph alpha">September 2008.</span>
This site is online.
</li>
</ul>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">July 2008.</span>
+ <span class="emph delta">July 2008.</span>
<a href="http://lambdadelta.info/documentation.html#ldJ1">First journal paper on λδ</a>
accepted for publication.
</li>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">July 2008.</span>
+ <span class="emph delta">July 2008.</span>
First <a href="http://helm.cs.unibo.it/procedural/">procedural reconstruction</a>
for <a href="http://matita.cs.unibo.it/">Matita 0.5</a>
of the λδ version 1 for Coq 7.3.1.
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">June 2008.</span>
+ <span class="emph delta">June 2008.</span>
The <a href="http://lambdadelta.info/version_1.html#static">
HTML pages of the specification of λδ version 1 for Matita 0.5</a>
are online.
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">May 2008.</span>
- The specification of λδ version 1 is dismissed.
+ <span class="emph delta">May 2008.</span>
+ The specification of λδ version 1 is concluded.
</li>
</ul>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">March 2008.</span>
+ <span class="emph alpha">March 2008.</span>
The specification of λδ version 2 is started with Coq 7.3.1 (false start).
</li>
</ul>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">September 2007.</span>
+ <span class="emph gamma">September 2007.</span>
The <a href="http://lambdadelta.info/version_1.html#dynamic">
specification of λδ version 1 for Matita 0.4</a>
is online.
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">November 2006.</span>
+ <span class="emph gamma">November 2006.</span>
<a href="http://lambdadelta.info/documentation.html#ldR2">λδ version 1</a>
is released.
</li>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">December 2005.</span>
+ <span class="emph beta">December 2005.</span>
<a href="http://lambdadelta.info/documentation.html#ldP1">First communication on λδ version 1</a>.
</li>
</ul>
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">May 2004.</span>
+ <span class="emph alpha">May 2004.</span>
The specification of <a href="http://lambdadelta.info/version_1.html">λδ version 1</a>
is started with Coq 7.3.1.
</li>
- <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="citations">Citations <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b3.png" />
- </div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
- This is a list of publications citing λδ (not including our own).
- </div>
-
- <ul xmlns:ld="http://lambdadelta.info/" id="C6">
- <li>
- A. Asperti, W. Ricciotti, C. Sacerdoti Coen, E. Tassi:
- <span class="date">Formal metatheory of programming languages in the Matita interactive theorem prover</span>
- (2012). In JAR 49(3), pp. 427-451.
- </li>
- </ul>
-
- <ul xmlns:ld="http://lambdadelta.info/" id="C5">
- <li>
- M.E. Maietti:
- <span class="date">Consistency of the minimalist foundation with Church thesis and Bar Induction</span>
- (2012). Submitted article.
- </li>
- </ul>
-
- <ul xmlns:ld="http://lambdadelta.info/" id="C4">
- <li>
- W. Ricciotti:
- <span class="date">Theoretical and implementation aspects in the mechanization of the metatheory of programming languages</span>
- (July 2011). Ph.D. Thesis in Computer Science, Technical Report UBLCS-2011-09, University of Bologna.
- </li>
- </ul>
-
- <ul xmlns:ld="http://lambdadelta.info/" id="C3">
- <li>
- C.E. Brown:
- <span class="date">Faithful Reproductions of the Automath Landau Formalization</span>
- (2011). Typescript note.
- </li>
- </ul>
-
- <ul xmlns:ld="http://lambdadelta.info/" id="C2">
- <li>
- M.E. Maietti:
- <span class="date">A minimalist two-level foundation for constructive mathematics</span>
- (2009). In APAL 160(3), pp. 319-354.
- </li>
- </ul>
-
- <ul xmlns:ld="http://lambdadelta.info/" id="C1">
- <li>
- V. Rahili:
- <span class="date">First Year Report: Realisability methods of proof and semantics with application to expansion</span>
- (July 2007). Typescript note.
- </li>
- </ul>
-
-
-
<div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="visibility">Visibility <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="date">June 2014.</span>
+ <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.
<ul xmlns:ld="http://lambdadelta.info/">
<li>
- <span class="date">June 2014.</span>
+ <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.
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 22 Oct 2014 20:00:28 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 28 Oct 2014 17:45:56 +0100</div>
</body>
</html>
</tr>
<tr>
<td class="snss capitalize sky">
- <a href="http://lambdadelta.info/index.html#notice">notice</a>
+ <a href="http://lambdadelta.info/index.html#citations">citations</a>
</td>
<td class="snss capitalize magenta">
- <a href="http://lambdadelta.info/news.html#citations">citations</a>
+ <a href="http://lambdadelta.info/news.html#visibility">visibility</a>
</td>
<td class="snss capitalize orange">
<a href="http://lambdadelta.info/documentation.html#v1">version 1</a>
<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:
+ which includes the major milestones.
+ </div>
+ <div xmlns:ld="http://lambdadelta.info/" class="text">
+ The life cycle of a specification consists of four periods.
+ <span class="emph alpha">Alpha:</span>
+ the definitions are designed and the major propositions are proved,
+ then the calculus is announced with a presentation.
+ <span class="emph beta">Beta:</span>
+ major changes and additions may occur before the calculus is released on paper.
+ <span class="emph gamma">Gamma:</span>
+ subsequent improvements occur until the specification is completed or superseded,
+ while major changes and additions are announced and reported on paper.
+ <span class="emph delta">Delta:</span>
+ after its conclusion, the specification is modified just for maintenance.
</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
<table cellpadding="4" cellspacing="0">
<td class="snnn top capitalize italic gray">started</td>
<td class="snnn top capitalize italic gray">announced</td>
<td class="snnn top capitalize italic gray">released</td>
- <td class="ssnn top capitalize italic gray">dismissed</td>
+ <td class="ssnn top capitalize italic gray">concluded</td>
</tr>
<tr>
<td class="snns top orange">
<td class="snnn top orange">April 2011</td>
<td class="snnn top orange">June 2014</td>
<td class="snnn top orange">October 2014</td>
- <td class="ssnn top orange">No</td>
+ <td class="ssnn top orange" />
+ </tr>
+ <tr>
+ <td class="snns top orange">Abandoned</td>
+ <td class="snnn top orange" />
+ <td class="snnn top orange">
+ <a href="http://coq.inria.fr/">Coq 7.3.1</a>
+ </td>
+ <td class="snnn top orange" />
+ <td class="snnn top orange">March 2008</td>
+ <td class="snnn top orange" />
+ <td class="snnn top orange" />
+ <td class="ssnn top orange">February 2011</td>
</tr>
<tr>
<td class="snss top red">
<div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="v2">
- <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" /> λδ version 2 (ongoing)</div>
+ <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" /> λδ version 2 (active)</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
The formal specification of λδ version 2
is available in the following formats:
<li>
<div class="text">
<a href="http://lambdadelta.info/download/lambdadelta_2.tar.gz">lambdadelta_2 for Matita 0.99.2</a>
- (revised <span class="date">2014-10</span>).
+ (revised <span class="emph gamma">2014-10</span>).
Source scripts.
</div>
<div class="text">
The scripts are grouped in directories, first by part, then by component.
</div>
<div class="text">
- <span class="date">Notice:</span>
+ <span class="emph alpha">Notice:</span>
the scripts are checked by the latest version of Matita from
<a href="http://matita.cs.unibo.it/download.shtml">HELM Subversion repository</a>
at path <trunk/matita/>.
<a href="http://lambdadelta.info/apps_2.html">Applications</a>.
</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
- <span class="date">Notice on numerical acounts:</span>
+ <span class="emph alpha">Notice on numerical acounts:</span>
nodes are counted according to the "intrinsic complexity measure"
[F. Guidi: "Procedural Representation of CIC Proof Terms"
Journal of Automated Reasoning 44(1-2), Springer (February 2010), pp. 53-78].
</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="text">
+ <span class="emph alpha">Notice on displayed logical structures:</span>
+ from the logical standpoint, the source scripts are grouped in "planes"
+ and these are grouped in "components";
+ the notation for the relations or functions
+ introduced in each script, is shown in parentheses (? are placeholders).
+ </div>
<div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="v1">
- <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b6.png" /> λδ version 1 (dismissed)</div>
+ <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b6.png" /> λδ version 1 (superseded)</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
The formal specification of λδ version 1
is available in the following formats:
<li>
<div class="text">
<a href="http://lambdadelta.info/download/lambdadelta_1.tar.gz">lambdadelta_1 for Coq 7.3.1</a>
- (revised <span class="date">2012-10</span>).
+ (revised <span class="emph delta">2012-10</span>).
Source scripts.
</div>
<div class="text">
<ul xmlns:ld="http://lambdadelta.info/" id="static1">
<li>
<a href="http://lambdadelta.info/static/matita/lambdadelta/">lambdadelta_1 for Matita 0.5</a>
- (revised <span class="date">2011-09</span>).
+ (revised <span class="emph delta">2011-09</span>).
Static HTML pages generated by the <a href="http://helm.cs.unibo.it/">HELM</a> rendering engine.
<ul>
<li>
<li>
<a href="http://mowgli.cs.unibo.it:58080/apply?keys=RT&xmluri=http://helm.cs.unibo.it/helm//html/folder/index.html&prop.media-type=text/html&param.thmedia-type=text/html&param.thkeys=T1%2CT2%2CL%2CE&param.embedkeys=d_c%2CTC1%2CHC2%2CL&param.thencoding=UTF-8&prop.encoding=UTF-8&prop.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&param.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&param.encoding=UTF-8&param.media-type=text/html&param.keys=d_c%2CC1%2CHC2%2CL&profile=default&param.profile=default&param.CICURI=theory:/matita/lambdadelta/">
lambdadelta_1 for Matita 0.5</a>
- (revised <span class="date">2011-09</span>).
+ (revised <span class="emph delta">2011-09</span>).
<a href="http://helm.cs.unibo.it/">HELM</a> directory.
- <span class="date">Notice: the HELM rendering engine is offline.</span>
+ <span class="emph alpha">Notice: the HELM rendering engine is offline.</span>
</li>
</ul>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 22 Oct 2014 20:08:56 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 28 Oct 2014 17:45:56 +0100</div>
</body>
</html>
<section4 name="bibtex">Documentation</section4>
<body>
BibTeX database of λδ documentation:
- <date date="download"/>
+ <notice class="alpha" notice="download"/>
<rlink to="download/lambdadelta.bib">lambdadelta.bib</rlink>,
- <date date="view"/>
+ <notice class="alpha" notice="view"/>
<rlink to="download/lambdadelta.txt">lambdadelta.txt</rlink>
- (revised <date date="2014-10"/>).
+ (revised <notice class="gamma" notice="2014-10"/>).
</body>
- <subsection name="v2"><version2-icon/>λδ version 2 (ongoing)</subsection>
+ <subsection name="v2"><version2-icon/>λδ version 2 (active)</subsection>
<body>
- The main source of information is <date date="P8"/>.
+ The main source of information is <notice class="alpha" notice="P8"/>.
</body>
<table name="documentation_2"/>
- <subsection name="v1"><version1-icon/>λδ version 1 (dismissed)</subsection>
+ <subsection name="v1"><version1-icon/>λδ version 1 (superseded)</subsection>
<body>
- The main source of information is <date date="J1"/>.
- A summary is available in <date date="P5"/>.
+ The main source of information is <notice class="alpha" notice="J1"/>.
+ A summary is available in <notice class="alpha" notice="P5"/>.
</body>
<table name="documentation_1"/>
name "documentation_1"
table {
- [ { name "ldJ1" "<span class=\"date\">J1.</span>" "" } {
+ [ { name "ldJ1" "<span class=\"emph alpha\">J1.</span>" "" } {
"F. Guidi:" +
@("http://doi.acm.org/10.1145/1614431.1614436"
"The Formal System λδ") +
- "(<span class=\"date\">2009-11</span>)." +
+ "(<span class=\"emph delta\">2009-11</span>)." +
"In ACM ToCL 11(1), pp. 5:1-5:37 (" ^
@("http://tocl.acm.org/accepted/335guidi.pdf" "accepted") +
- "<span class=\"date\">2008-07</span>)." +
+ "<span class=\"emph delta\">2008-07</span>)." +
"CoRR identifier" +
@("http://arxiv.org/abs/cs/0611040" "cs/0611040") +
"[v10] (revised" +
- "<span class=\"date\">2008-09</span>)." +
+ "<span class=\"emph delta\">2008-09</span>)." +
@@("documentation.html#bibtex" "BibTeX entry") ^ "."
* }
]
- [ { name "ldR3" "<span class=\"date\">R3.</span>" "" } {
+ [ { name "ldR3" "<span class=\"emph alpha\">R3.</span>" "" } {
"F. Guidi:" +
@@("download/cie_2007.pdf"
"Lambda Types on the Lambda Calculus with Abbreviations") +
- "(<span class=\"date\">2007-06</span>)." +
+ "(<span class=\"emph delta\">2007-06</span>)." +
"In CiE 2007 Local Proceedings." +
"University of Siena, technical report 487, p. 387" +
"(abstract of a presentation)." +
@@("documentation.html#bibtex" "BibTeX entry") ^ "."
* }
]
- [ { name "ldR2" "<span class=\"date\">R2.</span>" "" } {
+ [ { name "ldR2" "<span class=\"emph alpha\">R2.</span>" "" } {
"F. Guidi:" +
@("http://www.informatica.unibo.it/it/ricerca/technical-report/2006/UBLCS-2006-25"
"Lambda Types on the Lambda Calculus with Abbreviations") +
- "(<span class=\"date\">2006-11</span>)." +
+ "(<span class=\"emph gamma\">2006-11</span>)." +
"University of Bologna, technical report UBLCS-2006-25." +
@@("documentation.html#bibtex" "BibTeX entry") ^ "."
* }
]
- [ { name "ldR1" "<span class=\"date\">R1.</span>" "" } {
+ [ { name "ldR1" "<span class=\"emph alpha\">R1.</span>" "" } {
"F. Guidi:" +
@("http://www.informatica.unibo.it/it/ricerca/technical-report/2006/UBLCS-2006-01"
"Lambda Types on the Lambda Calculus with Abbreviations: a Certified Specification") +
- "(<span class=\"date\">2006-01</span>)." +
+ "(<span class=\"emph beta\">2006-01</span>)." +
"University of Bologna, technical report UBLCS-2006-01." +
@@("documentation.html#bibtex" "BibTeX entry") ^ "."
* }
]
- [ { name "ldP5" "<span class=\"date\">P5.</span>" "" } {
+ [ { name "ldP5" "<span class=\"emph alpha\">P5.</span>" "" } {
"F. Guidi:" +
@@("download/ld_talk_5s.pdf" "The Formal System λδ") +
- "(<span class=\"date\">2008-10</span>)." +
+ "(<span class=\"emph delta\">2008-10</span>)." +
"Presentation at Advances in Constructive Topology and Logical Foundations (slides)."
* }
]
- [ { name "ldP4" "<span class=\"date\">P4.</span>" "" } {
+ [ { name "ldP4" "<span class=\"emph alpha\">P4.</span>" "" } {
"F. Guidi:" +
@@("download/ld_talk_4s.pdf"
"Towards the Unification of Terms, Types and Contexts") +
- "(<span class=\"date\">2008-03</span>)." +
+ "(<span class=\"emph gamma\">2008-03</span>)." +
"Presentation at Types 2008 (slides)."
* }
]
- [ { name "ldP3" "<span class=\"date\">P3.</span>" "" } {
+ [ { name "ldP3" "<span class=\"emph alpha\">P3.</span>" "" } {
"F. Guidi:" +
@@("download/ld_talk_3s.pdf"
"Lambda Types on the Lambda Calculus with Abbreviations") +
- "(<span class=\"date\">2007-06</span>)." +
+ "(<span class=\"emph gamma\">2007-06</span>)." +
"Presentation at CiE 2007 (slides)."
* }
]
- [ { name "ldP2" "<span class=\"date\">P2.</span>" "" } {
+ [ { name "ldP2" "<span class=\"emph alpha\">P2.</span>" "" } {
"F. Guidi:" +
@@("download/ld_talk_2s.pdf"
"Lambda Tipi sul Lambda Calcolo con Abbreviazioni") +
- "(<span class=\"date\">2007-01</span>)." +
+ "(<span class=\"emph gamma\">2007-01</span>)." +
"Presentation at University of Padova (slides" +
- "<span class=\"date\">in Italian</span>)."
+ "<span class=\"emph alpha\">in Italian</span>)."
* }
]
- [ { name "ldP1" "<span class=\"date\">P1.</span>" "" } {
+ [ { name "ldP1" "<span class=\"emph alpha\">P1.</span>" "" } {
"F. Guidi:" +
@@("download/ld_talk_1s.pdf"
"Lambda Tipi sul Lambda Calcolo con Abbreviazioni: una Specifica Certificata") +
- "(<span class=\"date\">2005-12</span>)." +
+ "(<span class=\"emph beta\">2005-12</span>)." +
"Presentation at University of Bologna (slides" +
- "<span class=\"date\">in Italian</span>)."
+ "<span class=\"emph alpha\">in Italian</span>)."
* }
]
- [ { name "ldV1" "<span class=\"date\">V1.</span>" "" } {
+ [ { name "ldV1" "<span class=\"emph alpha\">V1.</span>" "" } {
"F. Guidi:" +
@@("version_1.html" "lambdadelta_1") +
- "(revised <span class=\"date\">2012-10</span>)." +
+ "(revised <span class=\"emph delta\">2012-10</span>)." +
"Formal specification for the proof assistant Coq 7.3.1 (scripts)." +
@@("documentation.html#bibtex" "BibTeX entry") ^ "."
* }
name "documentation_2"
table {
- [ { name "ldR5" "<span class=\"date\">R5.</span>" "" } {
+ [ { name "ldR5" "<span class=\"emph alpha\">R5.</span>" "" } {
"F. Guidi:" +
@@("download/cie_2010.pdf"
"An Efficient Validation Procedure for the Formal System λδ") +
- "(<span class=\"date\">2010-07</span>)." +
+ "(<span class=\"emph alpha\">2010-07</span>)." +
"In CiE 2010 Local Proceedings." +
"University of Azores, CMATI Booklet, pp. 204-213." +
@@("documentation.html#bibtex" "BibTeX entry") ^ "."
* }
]
- [ { name "ldR4" "<span class=\"date\">R4.</span>" "" } {
+ [ { name "ldR4" "<span class=\"emph alpha\">R4.</span>" "" } {
"F. Guidi:" +
@("http://www.informatica.unibo.it/it/ricerca/technical-report/2009/UBLCS-2009-16"
"Landau's \"Grundlagen der Analysis\" from Automath to lambda-delta") +
- "(<span class=\"date\">2009-09</span>)." +
+ "(<span class=\"emph alpha\">2009-09</span>)." +
"University of Bologna, technical report UBLCS-2009-16." +
@@("documentation.html#bibtex" "BibTeX entry") ^ "."
* }
]
- [ { name "ldP8" "<span class=\"date\">P8.</span>" "" } {
+ [ { name "ldP8" "<span class=\"emph alpha\">P8.</span>" "" } {
"F. Guidi:" +
@@("download/ld_talk_8s.pdf"
"The Formal System λδ and the \"Three Problems\"") +
- "(<span class=\"date\">2014-06</span>)." +
+ "(<span class=\"emph beta\">2014-06</span>)." +
"Presentation at University of Bologna (slides)."
* }
]
- [ { name "ldP7" "<span class=\"date\">P7.</span>" "" } {
+ [ { name "ldP7" "<span class=\"emph alpha\">P7.</span>" "" } {
"F. Guidi:" +
@@("download/ld_talk_7s.pdf"
"An Efficient Validation Procedure for the Formal System λδ") +
- "(<span class=\"date\">2010-07</span>)." +
+ "(<span class=\"emph alpha\">2010-07</span>)." +
"Presentation at CiE 2010 (slides)."
* }
]
- [ { name "ldP6" "<span class=\"date\">P6.</span>" "" } {
+ [ { name "ldP6" "<span class=\"emph alpha\">P6.</span>" "" } {
"F. Guidi:" +
@@("download/ld_talk_6s.pdf"
"A Validator for the Formal System λδ") +
- "(revised <span class=\"date\">2010-02</span>)." +
+ "(revised <span class=\"emph alpha\">2010-02</span>)." +
"Presentation at University of Bologna (slides)."
* }
]
- [ { name "ldV2" "<span class=\"date\">V2.</span>" "" } {
+ [ { name "ldV2" "<span class=\"emph alpha\">V2.</span>" "" } {
"F. Guidi:" +
@@("version_2.html" "lambdadelta_2") +
- "(revised <span class=\"date\">2014-10</span>)." +
+ "(revised <span class=\"emph gamma\">2014-10</span>)." +
"Formal specification for the proof assistant Matita 0.99.2 (scripts)." +
@@("documentation.html#bibtex" "BibTeX entry") ^ "."
* }
The λδ Digital Library is part of <link to="http://helm.cs.unibo.it/">HELM</link>
and contains resources expressed in λδ.
</body>
- <news date="Contents:">
+ <topitem name="contents">
+ <notice class="alpha" notice="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:">
+ </topitem>
+ <topitem name="access">
+ <notice class="alpha" notice="Access:"/>
+ <rlink to="static/lddl/">static pages</rlink> (updated <notice class="beta" notice="2012-10"/>),
+ <rlink to="download/lddl.tar.bz2">data set</rlink> (updated <notice class="beta" notice="2012-10"/>),
+ <rlink to="xml/">HELM server URL</rlink> (updated <notice class="beta" notice="2012-10"/>).
+ </topitem>
+ <topitem name="examples">
+ <notice class="alpha" notice="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>
+ </topitem>
<subsection name="helena"><helena-icon/>Helena</subsection>
<body>
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.">
+ <topitem name="v2">
+ <notice class="beta" notice="Version 0.8.2."/>
In progress.
- </news>
- <news date="Version 0.8.1 (2010-11).">
+ </topitem>
+ <topitem name="v1">
+ <notice class="beta" notice="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"
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"/>).
+ (revised <notice class="alpha" notice="2010-11"/>).
</item><item>
- <date date="2009-12."/>
+ <notice class="beta" notice="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).">
+ </topitem>
+ <topitem name="v0">
+ <notice class="beta" notice="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>.
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"/>).
+ (revised <notice class="gamma" notice="2008-07"/>).
</item><item>
- <date date="2009-09."/>
+ <notice class="beta" notice="2009-09."/>
Jutting's specification of Landau's "Grundlagen der Analysis"
enters λδ Digital Library.
</item><item>
- <date date="2009-06."/>
+ <notice class="beta" notice="2009-06."/>
Jutting's specification of Landau's "Grundlagen der Analysis"
is successfully processed, enabling sort inclusion.
</item></list>
- </news>
+ </topitem>
<footer/>
</page>
</body>
<body>
This is the System logo: <rlink to="images/crux_177.png">crux_177.png</rlink>
- (revised <date date="2012-09"/>).
+ (revised <notice class="alpha" notice="2012-09"/>).
</body>
-
- <section9 name="notice">Notice for the Internet Explorer user</section9>
<body>
+ <notice class="alpha" notice="Notice for the user of Internet Explorer."/>
To view this site correctly, please select a font
with <link to="http://www.unicode.org/">Unicode</link> support.
For example "Lucida Sans Unicode" (it should be already installed on your system).
"Tools" menu → "Internet Options" entry → "General" tab → "Fonts" button.
</body>
+<!-- ===================================================================== -->
+
+ <section9 name="citations">Citations</section9>
+ <body>
+ This is a list of publications citing λδ (not including our own).
+ </body>
+
+ <topitem name="C6">
+ A. Asperti, W. Ricciotti, C. Sacerdoti Coen, E. Tassi:
+ <notice class="alpha" notice="Formal metatheory of programming languages in the Matita interactive theorem prover"/>
+ (2012). In JAR 49(3), pp. 427-451.
+ </topitem>
+
+ <topitem name="C5">
+ M.E. Maietti:
+ <notice class="alpha" notice="Consistency of the minimalist foundation with Church thesis and Bar Induction"/>
+ (2012). Submitted article.
+ </topitem>
+
+ <topitem name="C4">
+ W. Ricciotti:
+ <notice class="alpha" notice="Theoretical and implementation aspects in the mechanization of the metatheory of programming languages"/>
+ (July 2011). Ph.D. Thesis in Computer Science, Technical Report UBLCS-2011-09, University of Bologna.
+ </topitem>
+
+ <topitem name="C3">
+ C.E. Brown:
+ <notice class="alpha" notice="Faithful Reproductions of the Automath Landau Formalization"/>
+ (2011). Typescript note.
+ </topitem>
+
+ <topitem name="C2">
+ M.E. Maietti:
+ <notice class="alpha" notice="A minimalist two-level foundation for constructive mathematics"/>
+ (2009). In APAL 160(3), pp. 319-354.
+ </topitem>
+
+ <topitem name="C1">
+ V. Rahili:
+ <notice class="alpha" notice="First Year Report: Realisability methods of proof and semantics with application to expansion"/>
+ (July 2007). Typescript note.
+ </topitem>
+
<footer/>
</page>
<section3 name="milestones">Milestones</section3>
- <news date="July 2014.">
+ <news class="beta" date="July 2014.">
A new version of this site is online.
</news>
- <news date="June 2014.">
+ <news class="beta" date="June 2014.">
<rlink to="documentation.html#ldP8">First communication on λδ version 2.</rlink>
</news>
- <news date="December 2012.">
+ <news class="alpha" date="December 2012.">
The character "_" is removed from the denomination "lambda_delta":
<list><item>
The denomination "\lambda\delta" is used in λδ-related texts.
</item></list>
</news>
- <news date="September 2011.">
+ <news class="alpha" date="September 2011.">
The denomination "lambda-delta" changes to "lambda_delta":
<list><item>
The character "-" is reserved in λδ textual syntax
</item></list>
</news>
- <news date="April 2011.">
+ <news class="alpha" date="April 2011.">
The specification of <rlink to="version_2.html">λδ version 2</rlink>
and related topics is restarted in
<link to="http://matita.cs.unibo.it/">Matita 0.5</link>.
</news>
- <news date="December 2010.">
+ <news class="delta" date="February 2011.">
+ The specification of λδ version 2 with Coq 7.3.1 is abandoned.
+ </news>
+
+ <news class="alpha" date="December 2010.">
Transient λδ URL acquired: http://lambda-delta.info/ (expires on December 2012).
</news>
- <news date="November 2010.">
+ <news class="beta" date="November 2010.">
"Helena 0.8.1" is released.
</news>
- <news date="September 2009.">
+ <news class="beta" date="September 2009.">
"Helena 0.8.0" is released and the
<rlink to="implementation.html#lddl">λδ Digital Library</rlink>
is started.
</news>
- <news date="June 2009.">
+ <news class="alpha" date="June 2009.">
"Helena", a <rlink to="implementation.html#helena">validator for λδ version 2</rlink>,
is available as a part of the <link to="http://helm.cs.unibo.it/">HELM</link> software.
</news>
- <news date="September 2008.">
+ <news class="alpha" date="September 2008.">
This site is online.
</news>
- <news date="July 2008.">
+ <news class="delta" date="July 2008.">
<rlink to="documentation.html#ldJ1">First journal paper on λδ</rlink>
accepted for publication.
</news>
- <news date="July 2008.">
+ <news class="delta" date="July 2008.">
First <link to="http://helm.cs.unibo.it/procedural/">procedural reconstruction</link>
for <link to="http://matita.cs.unibo.it/">Matita 0.5</link>
of the λδ version 1 for Coq 7.3.1.
</news>
- <news date="June 2008.">
+ <news class="delta" date="June 2008.">
The <rlink to="version_1.html#static">
HTML pages of the specification of λδ version 1 for Matita 0.5</rlink>
are online.
</news>
- <news date="May 2008.">
- The specification of λδ version 1 is dismissed.
+ <news class="delta" date="May 2008.">
+ The specification of λδ version 1 is concluded.
</news>
- <news date="March 2008.">
+ <news class="alpha" date="March 2008.">
The specification of λδ version 2 is started with Coq 7.3.1 (false start).
</news>
- <news date="September 2007.">
+ <news class="gamma" date="September 2007.">
The <rlink to="version_1.html#dynamic">
specification of λδ version 1 for Matita 0.4</rlink>
is online.
</news>
- <news date="November 2006.">
+ <news class="gamma" date="November 2006.">
<rlink to="documentation.html#ldR2">λδ version 1</rlink>
is released.
</news>
- <news date="December 2005.">
+ <news class="beta" date="December 2005.">
<rlink to="documentation.html#ldP1">First communication on λδ version 1</rlink>.
</news>
- <news date="May 2004.">
+ <news class="alpha" date="May 2004.">
The specification of <rlink to="version_1.html">λδ version 1</rlink>
is started with Coq 7.3.1.
</news>
-<!-- ===================================================================== -->
-
- <section3 name="citations">Citations</section3>
- <body>
- This is a list of publications citing λδ (not including our own).
- </body>
-
- <topitem name="C6">
- A. Asperti, W. Ricciotti, C. Sacerdoti Coen, E. Tassi:
- <date date="Formal metatheory of programming languages in the Matita interactive theorem prover"/>
- (2012). In JAR 49(3), pp. 427-451.
- </topitem>
-
- <topitem name="C5">
- M.E. Maietti:
- <date date="Consistency of the minimalist foundation with Church thesis and Bar Induction"/>
- (2012). Submitted article.
- </topitem>
-
- <topitem name="C4">
- W. Ricciotti:
- <date date="Theoretical and implementation aspects in the mechanization of the metatheory of programming languages"/>
- (July 2011). Ph.D. Thesis in Computer Science, Technical Report UBLCS-2011-09, University of Bologna.
- </topitem>
-
- <topitem name="C3">
- C.E. Brown:
- <date date="Faithful Reproductions of the Automath Landau Formalization"/>
- (2011). Typescript note.
- </topitem>
-
- <topitem name="C2">
- M.E. Maietti:
- <date date="A minimalist two-level foundation for constructive mathematics"/>
- (2009). In APAL 160(3), pp. 319-354.
- </topitem>
-
- <topitem name="C1">
- V. Rahili:
- <date date="First Year Report: Realisability methods of proof and semantics with application to expansion"/>
- (July 2007). Typescript note.
- </topitem>
-
<!-- ===================================================================== -->
<section3 name="visibility">Visibility</section3>
- <news date="June 2014.">
+ <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.
</news>
- <news date="June 2014.">
+ <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.
class "sky" {
[ @@("index" "home") * ]
[ @@("index#foreword" "foreword") * ]
- [ @@("index#notice" "notice") * ]
+ [ @@("index#citations" "citations") * ]
}
class "magenta" {
[ @@"news" * ]
[ @@("news#milestones" "milestones") * ]
- [ @@("news#citations" "citations") * ]
+ [ @@("news#visibility" "visibility") * ]
}
class "orange" {
[ @@"documentation" * ]
<body>
λδ is developed as a machine-checked digital specification.
It comes in several versions listed in the next table,
- which includes the major milestones:
+ which includes the major milestones.
+ </body>
+ <body>
+ The life cycle of a specification consists of four periods.
+ <notice class="alpha" notice="Alpha:"/>
+ the definitions are designed and the major propositions are proved,
+ then the calculus is announced with a presentation.
+ <notice class="beta" notice="Beta:"/>
+ major changes and additions may occur before the calculus is released on paper.
+ <notice class="gamma" notice="Gamma:"/>
+ subsequent improvements occur until the specification is completed or superseded,
+ while major changes and additions are announced and reported on paper.
+ <notice class="delta" notice="Delta:"/>
+ after its conclusion, the specification is modified just for maintenance.
</body>
<table name="versions"/>
<!-- VERSION 2 =========================================================== -->
- <subsection name="v2"><version2-icon/>λδ version 2 (ongoing)</subsection>
+ <subsection name="v2"><version2-icon/>λδ version 2 (active)</subsection>
<body>
The formal specification of λδ version 2
is available in the following formats:
<topitem name="source2">
<body>
<rlink to="download/lambdadelta_2.tar.gz">lambdadelta_2 for Matita 0.99.2</rlink>
- (revised <date date="2014-10"/>).
+ (revised <notice class="gamma" notice="2014-10"/>).
Source scripts.
</body>
<body>
The scripts are grouped in directories, first by part, then by component.
</body>
<body>
- <date date="Notice:"/>
+ <notice class="alpha" notice="Notice:"/>
the scripts are checked by the latest version of Matita from
<link to="http://matita.cs.unibo.it/download.shtml">HELM Subversion repository</link>
at path <trunk/matita/>.
<rlink to="apps_2.html">Applications</rlink>.
</body>
<body>
- <date date="Notice on numerical acounts:"/>
+ <notice class="alpha" notice="Notice on numerical acounts:"/>
nodes are counted according to the "intrinsic complexity measure"
[F. Guidi: "Procedural Representation of CIC Proof Terms"
Journal of Automated Reasoning 44(1-2), Springer (February 2010), pp. 53-78].
</body>
+ <body>
+ <notice class="alpha" notice="Notice on displayed logical structures:"/>
+ from the logical standpoint, the source scripts are grouped in "planes"
+ and these are grouped in "components";
+ the notation for the relations or functions
+ introduced in each script, is shown in parentheses (? are placeholders).
+ </body>
<!-- VERSION 1 =========================================================== -->
- <subsection name="v1"><version1-icon/>λδ version 1 (dismissed)</subsection>
+ <subsection name="v1"><version1-icon/>λδ version 1 (superseded)</subsection>
<body>
The formal specification of λδ version 1
is available in the following formats:
<topitem name="source1">
<body>
<rlink to="download/lambdadelta_1.tar.gz">lambdadelta_1 for Coq 7.3.1</rlink>
- (revised <date date="2012-10"/>).
+ (revised <notice class="delta" notice="2012-10"/>).
Source scripts.
</body>
<body>
<topitem name="static1">
<rlink to="static/matita/lambdadelta/">lambdadelta_1 for Matita 0.5</rlink>
- (revised <date date="2011-09"/>).
+ (revised <notice class="delta" notice="2011-09"/>).
Static HTML pages generated by the <link to="http://helm.cs.unibo.it/">HELM</link> rendering engine.
<list><item>
<rlink to="static/matita/lambdadelta/basic_1/pr3/pr3/pr3_confluence.con.html">
<topitem name="dynamic1">
<link to="http://mowgli.cs.unibo.it:58080/apply?keys=RT&xmluri=http://helm.cs.unibo.it/helm//html/folder/index.html&prop.media-type=text/html&param.thmedia-type=text/html&param.thkeys=T1%2CT2%2CL%2CE&param.embedkeys=d_c%2CTC1%2CHC2%2CL&param.thencoding=UTF-8&prop.encoding=UTF-8&prop.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&param.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&param.encoding=UTF-8&param.media-type=text/html&param.keys=d_c%2CC1%2CHC2%2CL&profile=default&param.profile=default&param.CICURI=theory:/matita/lambdadelta/">
lambdadelta_1 for Matita 0.5</link>
- (revised <date date="2011-09"/>).
+ (revised <notice class="delta" notice="2011-09"/>).
<link to="http://helm.cs.unibo.it/">HELM</link> directory.
- <date date="Notice: the HELM rendering engine is offline."/>
+ <notice class="alpha" notice="Notice: the HELM rendering engine is offline."/>
</topitem>
<footer/>
table {
class "gray"
[ "version" "name" "developed with"
- "stage" "started" "announced" "released" "dismissed"
+ "stage" "started" "announced" "released" "concluded"
]
class "orange"
[ @@("specification#v2" "Version 2") "\"basic_2\"" @("http://matita.cs.unibo.it/" "Matita 0.99.2")
- "\"A\"" "April 2011" "June 2014" "October 2014" "No"
+ "\"A\"" "April 2011" "June 2014" "October 2014" ""
+ ]
+ class "orange"
+ [ "Abandoned" "" @("http://coq.inria.fr/" "Coq 7.3.1")
+ "" "March 2008" "" "" "February 2011"
]
class "red"
[ @@("specification#v1" "Version 1") "\"basic_1\"" @("http://coq.inria.fr/" "Coq 7.3.1")
<xsl:template match="ld:news">
<ul><li>
- <span class="date"><xsl:value-of select="@date"/></span>
+ <span class="emph {@class}"><xsl:value-of select="@date"/></span>
<xsl:apply-templates/>
</li></ul>
</xsl:template>
<li><xsl:apply-templates/></li>
</xsl:template>
-<xsl:template match="ld:date">
- <span class="date"><xsl:value-of select="@date"/></span>
+<xsl:template match="ld:notice">
+ <span class="emph {@class}"><xsl:value-of select="@notice"/></span>
</xsl:template>
<xsl:template match="ld:version2-icon">
projects / helm.git / commitdiff