<table cellpadding="4" cellspacing="0">
<tbody>
<tr>
- <td class="snns component sky">
- <a href="http://lambdadelta.info/index.html">foreword</a>
+ <td class="snns capitalize italic sky">
+ <a href="http://lambdadelta.info/index.html">home</a>
</td>
- <td class="snns component magenta">
+ <td class="snns capitalize italic magenta">
<a href="http://lambdadelta.info/news.html">news</a>
</td>
- <td class="snns component orange">
+ <td class="snns capitalize italic orange">
<a href="http://lambdadelta.info/documentation.html">documentation</a>
</td>
- <td class="snns component green">
+ <td class="snns capitalize italic green">
<a href="http://lambdadelta.info/implementation.html">implementation</a>
</td>
- <td class="snnn component green">
- <br />
- </td>
- <td class="snnn component green">
- <br />
- </td>
- <td class="ssnn component green">
- <br />
- </td>
+ <td class="ssnn capitalize italic green">(<a href="http://lambdadelta.info/implementation.html#specifications">specifications</a> - <a href="http://lambdadelta.info/implementation.html#lddl">library</a> - <a href="http://lambdadelta.info/implementation.html#helena">Helena</a>)</td>
</tr>
<tr>
<td class="snns sky">
- <br />
+ <a href="http://lambdadelta.info/index.html#foreword">Foreword</a>
</td>
<td class="snns magenta">
- <br />
+ <a href="http://lambdadelta.info/news.html#milestones">Milestones</a>
</td>
<td class="snns orange">
- <br />
+ <a href="http://lambdadelta.info/documentation.html#v2">Version 2</a>
</td>
<td class="snns green">
<a href="http://lambdadelta.info/version_2.html">Version 2</a>
</td>
- <td class="snnn green">
- <a href="http://lambdadelta.info/ground_2.html">Background</a>
- </td>
- <td class="snnn green">
- <a href="http://lambdadelta.info/basic_2.html">Core</a>
- </td>
- <td class="ssnn green">
- <a href="http://lambdadelta.info/apps_2.html">Applications</a>
- </td>
+ <td class="ssnn 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>
</tr>
<tr>
- <td class="nnss sky">
- <br />
+ <td class="snss sky">
+ <a href="http://lambdadelta.info/index.html#notice">Notice</a>
</td>
- <td class="nnss magenta">
- <br />
+ <td class="snss magenta">
+ <a href="http://lambdadelta.info/news.html#visibility">Visibility</a>
</td>
- <td class="nnss orange">
- <br />
+ <td class="snss orange">
+ <a href="http://lambdadelta.info/documentation.html#v1">Version 1</a>
</td>
<td class="snss green">
<a href="http://lambdadelta.info/version_1.html">Version 1</a>
</td>
- <td class="snsn green">
- <br />
- </td>
- <td class="snsn green">
- <br />
- </td>
<td class="sssn green">
<br />
</td>
</table>
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="foreword">Formats <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b9.png" />
+ <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="foreword">Formats <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b6.png" />
</div>
+
<div xmlns:ld="http://lambdadelta.info/" class="text">
The formal specification of λδ version 1
is available in the following formats:
+ </div>
+
+ <ul xmlns:ld="http://lambdadelta.info/" id="source">
+ <li>
+ <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>).
+ Source scripts.
+ </li>
+ </ul>
+
+ <ul xmlns:ld="http://lambdadelta.info/" id="static">
+ <li>
+ <a href="http://lambdadelta.info/static/matita/lambdadelta/">lambdadelta_1 for Matita 0.5"</a>
+ (revised <span class="date">2011-09</span>).
+ Static HTML pages generated by the <a href="http://helm.cs.unibo.it/">HELM</a> rendering engine.
<ul>
- <li>
- <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>).
- Source scripts.
- <a href="http://lambdadelta.info/implementation.html#bibtex">BibTeX entry</a>
+ <li>
+ <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/pr3/pr3/pr3_confluence.con.html">
+ Confluence of reduction</a>
+ (Church-Rosser property).
</li>
- </ul>
- <ul>
- <li>
- <a href="http://lambdadelta.info/static/matita/lambdadelta/">lambdadelta_1 for Matita 0.5"</a>
- (revised <span class="date">2011-09</span>).
- Static HTML pages generated by the <a href="http://helm.cs.unibo.it/">HELM</a> rendering engine.
- <ul>
- <li>
- <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/pr3/pr3/pr3_confluence.con.html">
- Confluence of reduction</a>
- (Church-Rosser property).
- </li>
- <li>
- <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/props/ty3_correct.con.html">
- Correctness of types</a>.
- </li>
- <li>
- <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/props/ty3_unique.con.html">
- Uniqueness of types up to conversion</a>.
- </li>
- <li>
- <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/pr3/ty3_sred_pr3.con.html">
- Subject reduction of the type assignment</a>.
- </li>
- <li>
- <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/arity_props/ty3_sn3.con.html">
- Strong normalization of the typed terms</a>.
- </li>
- <li>
- <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/dec/ty3_inference.con.html">
- Decidability of the type inference problem</a>.
- </li>
- </ul>
+ <li>
+ <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/props/ty3_correct.con.html">
+ Correctness of types</a>.
</li>
- </ul>
- <ul>
- <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>).
- <a href="http://helm.cs.unibo.it/">HELM</a> directory.
- <span class="date">Notice: the HELM rendering engine is offline.</span>
+ <li>
+ <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/props/ty3_unique.con.html">
+ Uniqueness of types up to conversion</a>.
</li>
- </ul>
- </div>
+ <li>
+ <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/pr3/ty3_sred_pr3.con.html">
+ Subject reduction of the type assignment</a>.
+ </li>
+ <li>
+ <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/arity_props/ty3_sn3.con.html">
+ Strong normalization of the typed terms</a>.
+ </li>
+ <li>
+ <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/dec/ty3_inference.con.html">
+ Decidability of the type inference problem</a>.
+ </li>
+ </ul>
+ </li>
+ </ul>
+
+ <ul xmlns:ld="http://lambdadelta.info/" id="dynamic">
+ <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>).
+ <a href="http://helm.cs.unibo.it/">HELM</a> directory.
+ <span class="date">Notice: the HELM rendering engine is offline.</span>
+ </li>
+ </ul>
<div class="spacer">
<img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 06 Jul 2014 22:50:18 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 10 Sep 2014 14:46:05 +0200</div>
</body>
</html>
projects / helm.git / blobdiff