<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 15:02:32 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 16:13:31 +0200</div>
</body>
</html>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 15:02:32 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 16:13:31 +0200</div>
</body>
</html>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 15:02:32 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 16:13:31 +0200</div>
</body>
</html>
<td class="snns component green">
<a href="http://lambdadelta.info/implementation.html">implementation</a>
</td>
- <td class="ssnn component 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>
+ <td class="ssnn component 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">
<td class="snns green">
<a href="http://lambdadelta.info/version_2.html">Version 2</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>
+ <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="snss sky">
BibTeX database of λδ documentation:
<a href="http://lambdadelta.info/download/lambdadelta.bib">lambdadelta.bib</a>,
<a href="http://lambdadelta.info/download/lambdadelta.txt">lambdadelta.txt</a>
- (revised <span class="date">2012-10</span>).
+ (revised <span class="date">2014-07</span>).
</div>
<div xmlns:ld="http://lambdadelta.info/" class="head2sn" id="v2">
<table cellpadding="4" cellspacing="0">
<tbody>
<tr>
- <td class="snns top" id="ldp7">
+ <td class="snns top" id="ldR5">
<span class="date">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>
</tr>
<tr>
- <td class="snns top" id="ldp6">
+ <td class="snns top" id="ldR4">
<span class="date">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>
</tr>
<tr>
- <td class="snns top" id="ldt8">
+ <td class="snns top" id="ldP8">
<span class="date">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>
</tr>
<tr>
- <td class="snns top" id="ldt7">
+ <td class="snns top" id="ldP7">
<span class="date">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>
</tr>
<tr>
- <td class="snns top" id="ldt6">
+ <td class="snns top" id="ldP6">
<span class="date">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>
<table cellpadding="4" cellspacing="0">
<tbody>
<tr>
- <td class="snns top" id="ldp5">
+ <td class="snns top" id="ldJ1">
<span class="date">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 In ACM ToCL 11(1), pp. 5:1-5:37 ( <a href="http://tocl.acm.org/accepted/335guidi.pdf">accepted</a>
</td>
</tr>
<tr>
- <td class="snns top" id="ldp4">
+ <td class="snns top" id="ldR3">
<span class="date">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>
</tr>
<tr>
- <td class="snns top" id="ldp3">
+ <td class="snns top" id="ldR2">
<span class="date">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>
</tr>
<tr>
- <td class="snns top" id="ldp2">
+ <td class="snns top" id="ldR1">
<span class="date">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>
</tr>
<tr>
- <td class="snns top" id="ldt5">
+ <td class="snns top" id="ldP5">
<span class="date">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>
</tr>
<tr>
- <td class="snns top" id="ldt4">
+ <td class="snns top" id="ldP4">
<span class="date">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>
</tr>
<tr>
- <td class="snns top" id="ldt3">
+ <td class="snns top" id="ldP3">
<span class="date">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>
</tr>
<tr>
- <td class="snns top" id="ldt2">
+ <td class="snns top" id="ldP2">
<span class="date">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>
</tr>
<tr>
- <td class="snns top" id="ldt1">
+ <td class="snns top" id="ldP1">
<span class="date">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>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 15:02:32 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 16:15:22 +0200</div>
</body>
</html>
% \lambda\delta version 2 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-@misc{lambdadelta8,
+@misc{lambdadeltaV2,
author="F. {Guidi}",
title="{lambdadelta\_2}",
howpublished="Formal specification for the proof assistant Matita 0.99.2",
note="Available at the $\lambda\delta$ Web site: $<$http://lambdadelta.info/$>$"
}
-@incollection{lambdadelta7,
+@incollection{lambdadeltaR5,
author="F. {Guidi}",
title="{An Efficient Validation Procedure for the Formal System $\lambda\delta$}",
editor="F. {Ferreira} and H. {Guerra} and E. {Mayordomo} and J. {Rasga}",
month="July"
}
-@techreport{lambdadelta6,
+@techreport{lambdadeltaR4,
author="F. {Guidi}",
title="{Landau's ``Grundlagen der Analysis'' from Automath to lambda-delta}",
type="Technical Report",
% \lambda\delta version 1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-@article{lambdadelta5,
+@article{lambdadeltaJ1,
author="F. {Guidi}",
title="{The Formal System $\lambda\delta$}",
journal="Transactions on Computational Logic",
month="November"
}
-@incollection{lambdadelta4,
+@incollection{lambdadeltaR3,
author="F. {Guidi}",
title="{Lambda Types on the Lambda Calculus with Abbreviations}",
editor="S. {Barry Cooper} and T. F. {Kent} and B. {L\"owe} and A. {Sorbi}", @comment="{\"}",
month="June"
}
-@techreport{lambdadelta3,
+@techreport{lambdadeltaR2,
author="F. {Guidi}",
title="{Lambda-Types on the Lambda-Calculus with Abbreviations}",
type="Technical Report",
month="November"
}
-@techreport{lambdadelta2,
+@techreport{lambdadeltaR1,
author="F. {Guidi}",
title="{Lambda-Types on the Lambda-Calculus with Abbreviations: a Certified Specification}",
type="Technical Report",
month="January"
}
-@misc{lambdadelta1,
+@misc{lambdadeltaV1,
author="F. {Guidi}",
title="{lambdadelta\_1}",
howpublished="Formal specification for the proof assistant Coq 7.3.1",
% \lambda\delta version 2 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-@misc{lambdadelta8,
+@misc{lambdadeltaV2,
author="F. {Guidi}",
title="{lambdadelta\_2}",
howpublished="Formal specification for the proof assistant Matita 0.99.2",
note="Available at the $\lambda\delta$ Web site: $<$http://lambdadelta.info/$>$"
}
-@incollection{lambdadelta7,
+@incollection{lambdadeltaR5,
author="F. {Guidi}",
title="{An Efficient Validation Procedure for the Formal System $\lambda\delta$}",
editor="F. {Ferreira} and H. {Guerra} and E. {Mayordomo} and J. {Rasga}",
month="July"
}
-@techreport{lambdadelta6,
+@techreport{lambdadeltaR4,
author="F. {Guidi}",
title="{Landau's ``Grundlagen der Analysis'' from Automath to lambda-delta}",
type="Technical Report",
% \lambda\delta version 1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-@article{lambdadelta5,
+@article{lambdadeltaJ1,
author="F. {Guidi}",
title="{The Formal System $\lambda\delta$}",
journal="Transactions on Computational Logic",
month="November"
}
-@incollection{lambdadelta4,
+@incollection{lambdadeltaR3,
author="F. {Guidi}",
title="{Lambda Types on the Lambda Calculus with Abbreviations}",
editor="S. {Barry Cooper} and T. F. {Kent} and B. {L\"owe} and A. {Sorbi}", @comment="{\"}",
month="June"
}
-@techreport{lambdadelta3,
+@techreport{lambdadeltaR2,
author="F. {Guidi}",
title="{Lambda-Types on the Lambda-Calculus with Abbreviations}",
type="Technical Report",
month="November"
}
-@techreport{lambdadelta2,
+@techreport{lambdadeltaR1,
author="F. {Guidi}",
title="{Lambda-Types on the Lambda-Calculus with Abbreviations: a Certified Specification}",
type="Technical Report",
month="January"
}
-@misc{lambdadelta1,
+@misc{lambdadeltaV1,
author="F. {Guidi}",
title="{lambdadelta\_1}",
howpublished="Formal specification for the proof assistant Coq 7.3.1",
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 15:02:32 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 16:13:31 +0200</div>
</body>
</html>
<td class="snns component green">
<a href="http://lambdadelta.info/implementation.html">implementation</a>
</td>
- <td class="ssnn component 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>
+ <td class="ssnn component 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">
<td class="snns green">
<a href="http://lambdadelta.info/version_2.html">Version 2</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>
+ <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="snss sky">
Exploits a subset of "complete_rg" λδ as the intermediate language.
Features importation from ".hln" files containing λδ textual syntax.
The overall validation speed of the "Grundlagen der Analysis"
- increases of 22% with respect toversion 0.8.0.
+ increases of 22% with respect to version 0.8.0.
[Svn revision: 11032] (<a href="http://lambdadelta.info/download/helena_0.8.1.tar.gz">archived source code</a>)
<ul>
<li>
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>.
- <a href="http://lambdadelta.info/documentation.html#ldp6">Documentation</a>.
+ <a href="http://lambdadelta.info/documentation.html#ldR4">Documentation (R4)</a>.
[Svn revision: 10304] (<a href="http://lambdadelta.info/download/helena_0.8.0.tar.gz">archived source code</a>).
<ul>
<li>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 15:02:32 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 16:13:31 +0200</div>
</body>
</html>
<td class="snns component green">
<a href="http://lambdadelta.info/implementation.html">implementation</a>
</td>
- <td class="ssnn component 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>
+ <td class="ssnn component 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">
<td class="snns green">
<a href="http://lambdadelta.info/version_2.html">Version 2</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>
+ <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="snss sky">
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 15:02:32 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 16:13:31 +0200</div>
</body>
</html>
<td class="snns component green">
<a href="http://lambdadelta.info/implementation.html">implementation</a>
</td>
- <td class="ssnn component 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>
+ <td class="ssnn component 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">
<td class="snns green">
<a href="http://lambdadelta.info/version_2.html">Version 2</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>
+ <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="snss sky">
<div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="milestones">Milestones <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b5.png" />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
- <ul>
- <li>
- <span class="date">June 2014.</span>
- <a href="http://lambdadelta.info/documentation.html#ldt8">First communication on λδ version 2.</a>
- </li>
- </ul>
- <ul>
- <li>
- <span class="date">December 2012.</span>
- The character "_" is removed from the denomination "lambda_delta":
- <ul>
- <li>
- The denomination "\lambda\delta" is used in λδ-related texts.
- </li>
- <li>
- The denomination "lambdadelta" is used in λδ-related identifiers.
- </li>
- <li>
- Permanent λδ URL acquired:
- <a href="http://lambdadelta.info/">http://lambdadelta.info/</a>
- (pointing at this site).
- </li>
- </ul>
- </li>
- </ul>
- <ul>
- <li>
- <span class="date">September 2011.</span>
- The denomination "lambda-delta" changes to "lambda_delta":
- <ul>
- <li>
- The character "-" is reserved in λδ textual syntax
- (recognized by "Helena 0.8.1").
- </li>
- <li>
- Eventually, the occurrences of the character "-"
- will be replaced by "_" in all λδ-related identifiers.
- </li>
- <li>
- In particular, this refactoring involves file names and path names.
- </li>
- </ul>
- </li>
- </ul>
- <ul>
- <li>
- <span class="date">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>.
- </li>
- </ul>
- <ul>
- <li>
- <span class="date">December 2010.</span>
- Transient λδ URL acquired: http://lambda-delta.info/ (expires on December 2012).
- </li>
- </ul>
- <ul>
- <li>
- <span class="date">November 2010.</span>
- "Helena 0.8.1" is released.
- </li>
- </ul>
- <ul>
- <li>
- <span class="date">September 2009.</span>
- "Helena 0.8.0" is released and the
- <a href="http://lambdadelta.info/implementation.html#lddl">λδ Digital Library</a>
- is started.
- </li>
- </ul>
- <ul>
- <li>
- <span class="date">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>
- <ul>
- <li>
- <span class="date">September 2008.</span>
- This site is online.
- </li>
- </ul>
- <ul>
- <li>
- <span class="date">July 2008.</span>
- <a href="http://lambdadelta.info/documentation.html#ldp5">First journal paper on λδ</a>
- accepted for publication.
- </li>
- </ul>
- <ul>
- <li>
- <span class="date">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.
- </li>
- </ul>
- <ul>
- <li>
- <span class="date">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.
- </li>
- </ul>
+
+ <ul xmlns:ld="http://lambdadelta.info/">
+ <li>
+ <span class="date">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>
+ <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>
+ The character "_" is removed from the denomination "lambda_delta":
<ul>
- <li>
- <span class="date">May 2008.</span>
- The specification of λδ version 1 is dismissed.
+ <li>
+ The denomination "\lambda\delta" is used in λδ-related texts.
</li>
- </ul>
- <ul>
- <li>
- <span class="date">March 2008.</span>
- The specification of λδ version 2 is started with Coq 7.3.1 (false start).
+ <li>
+ The denomination "lambdadelta" is used in λδ-related identifiers.
</li>
- </ul>
- <ul>
- <li>
- <span class="date">September 2007.</span>
- The <a href="http://lambdadelta.info/version_1.html#dynamic">
- specification of λδ version 1 for Matita 0.4</a>
- is online.
+ <li>
+ Permanent λδ URL acquired:
+ <a href="http://lambdadelta.info/">http://lambdadelta.info/</a>
+ (pointing at this site).
</li>
- </ul>
+ </ul>
+ </li>
+ </ul>
+
+ <ul xmlns:ld="http://lambdadelta.info/">
+ <li>
+ <span class="date">September 2011.</span>
+ The denomination "lambda-delta" changes to "lambda_delta":
<ul>
- <li>
- <span class="date">November 2006.</span>
- <a href="http://lambdadelta.info/documentation.html#ldp3">λδ version 1</a>
- is released.
+ <li>
+ The character "-" is reserved in λδ textual syntax
+ (recognized by "Helena 0.8.1").
</li>
- </ul>
- <ul>
- <li>
- <span class="date">December 2005.</span>
- <a href="http://lambdadelta.info/documentation.html#ldt1">First communication on λδ</a>.
+ <li>
+ Eventually, the occurrences of the character "-"
+ will be replaced by "_" in all λδ-related identifiers.
</li>
- </ul>
- <ul>
- <li>
- <span class="date">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>
+ In particular, this refactoring involves file names and path names.
</li>
- </ul>
- </div>
+ </ul>
+ </li>
+ </ul>
+
+ <ul xmlns:ld="http://lambdadelta.info/">
+ <li>
+ <span class="date">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>.
+ </li>
+ </ul>
+
+ <ul xmlns:ld="http://lambdadelta.info/">
+ <li>
+ <span class="date">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>
+ "Helena 0.8.1" is released.
+ </li>
+ </ul>
+
+ <ul xmlns:ld="http://lambdadelta.info/">
+ <li>
+ <span class="date">September 2009.</span>
+ "Helena 0.8.0" is released and the
+ <a href="http://lambdadelta.info/implementation.html#lddl">λδ Digital Library</a>
+ is started.
+ </li>
+ </ul>
+
+ <ul xmlns:ld="http://lambdadelta.info/">
+ <li>
+ <span class="date">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>
+
+ <ul xmlns:ld="http://lambdadelta.info/">
+ <li>
+ <span class="date">September 2008.</span>
+ This site is online.
+ </li>
+ </ul>
+
+ <ul xmlns:ld="http://lambdadelta.info/">
+ <li>
+ <span class="date">July 2008.</span>
+ <a href="http://lambdadelta.info/documentation.html#ldJ1">First journal paper on λδ</a>
+ accepted for publication.
+ </li>
+ </ul>
+
+ <ul xmlns:ld="http://lambdadelta.info/">
+ <li>
+ <span class="date">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.
+ </li>
+ </ul>
+
+ <ul xmlns:ld="http://lambdadelta.info/">
+ <li>
+ <span class="date">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.
+ </li>
+ </ul>
+
+ <ul xmlns:ld="http://lambdadelta.info/">
+ <li>
+ <span class="date">May 2008.</span>
+ The specification of λδ version 1 is dismissed.
+ </li>
+ </ul>
+
+ <ul xmlns:ld="http://lambdadelta.info/">
+ <li>
+ <span class="date">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>
+ The <a href="http://lambdadelta.info/version_1.html#dynamic">
+ specification of λδ version 1 for Matita 0.4</a>
+ is online.
+ </li>
+ </ul>
+
+ <ul xmlns:ld="http://lambdadelta.info/">
+ <li>
+ <span class="date">November 2006.</span>
+ <a href="http://lambdadelta.info/documentation.html#ldR2">λδ version 1</a>
+ is released.
+ </li>
+ </ul>
+
+ <ul xmlns:ld="http://lambdadelta.info/">
+ <li>
+ <span class="date">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>
+ The specification of <a href="http://lambdadelta.info/version_1.html">λδ version 1</a>
+ is started with Coq 7.3.1.
+ </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/b4.png" />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
- <ul>
- <li>
- <span class="date">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.
- </li>
- </ul>
- <ul>
- <li>
- <span class="date">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.
- </li>
- </ul>
- </div>
+
+ <ul xmlns:ld="http://lambdadelta.info/">
+ <li>
+ <span class="date">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.
+ </li>
+ </ul>
+
+ <ul xmlns:ld="http://lambdadelta.info/">
+ <li>
+ <span class="date">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.
+ </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, 20 Jul 2014 15:02:32 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 16:13:31 +0200</div>
</body>
</html>
<td class="snns component green">
<a href="http://lambdadelta.info/implementation.html">implementation</a>
</td>
- <td class="ssnn component 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>
+ <td class="ssnn component 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">
<td class="snns green">
<a href="http://lambdadelta.info/version_2.html">Version 2</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>
+ <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="snss sky">
<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:
- <ul 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.
+ </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/static/matita/lambdadelta/basic_1/pr3/pr3/pr3_confluence.con.html">
+ Confluence of reduction</a>
+ (Church-Rosser property).
</li>
- </ul>
- <ul 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/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 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>
+ <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, 20 Jul 2014 15:02:32 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 16:13:31 +0200</div>
</body>
</html>
<td class="snns component green">
<a href="http://lambdadelta.info/implementation.html">implementation</a>
</td>
- <td class="ssnn component 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>
+ <td class="ssnn component 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">
<td class="snns green">
<a href="http://lambdadelta.info/version_2.html">Version 2</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>
+ <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="snss sky">
<div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="foreword">Formats <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
</div>
+
<div xmlns:ld="http://lambdadelta.info/" class="text">
The formal specification of λδ version 2
is available in the following formats:
- <ul id="source">
- <li>
- <a href="http://lambdadelta.info/download/lambdadelta_2.tar.gz">lambdadelta_2 for Matita 0.99.2</a>
- (revised <span class="date">2014-07</span>).
- Source scripts.
- </li>
- </ul>
- <ul id="parts">
- <li>
- <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>.
- Informational pages on the parts of the specification.
- </li>
- </ul>
</div>
+ <ul xmlns:ld="http://lambdadelta.info/" id="source">
+ <li>
+ <a href="http://lambdadelta.info/download/lambdadelta_2.tar.gz">lambdadelta_2 for Matita 0.99.2</a>
+ (revised <span class="date">2014-07</span>).
+ Source scripts.
+ </li>
+ </ul>
+
+ <ul xmlns:ld="http://lambdadelta.info/" id="parts">
+ <li>
+ <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>.
+ Informational pages on the parts of the specification.
+ </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: Sun, 20 Jul 2014 15:02:32 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 16:13:31 +0200</div>
</body>
</html>
BibTeX database of λδ documentation:
<rlink to="download/lambdadelta.bib">lambdadelta.bib</rlink>,
<rlink to="download/lambdadelta.txt">lambdadelta.txt</rlink>
- (revised <date date="2012-10"/>).
+ (revised <date date="2014-07"/>).
</body>
<section name="v2"><basic-icon/>λδ version 2 (in progress)</section>
name "documentation_1"
table {
- [ { name "ldp5" "<span class=\"date\">J1.</span>" "" } {
+ [ { name "ldJ1" "<span class=\"date\">J1.</span>" "" } {
"F. Guidi:" +
@("http://doi.acm.org/10.1145/1614431.1614436"
"The Formal System λδ") +
@@("documentation.html#bibtex" "BibTeX entry") ^ "."
* }
]
- [ { name "ldp4" "<span class=\"date\">R3.</span>" "" } {
+ [ { name "ldR3" "<span class=\"date\">R3.</span>" "" } {
"F. Guidi:" +
@@("download/cie_2007.pdf"
"Lambda Types on the Lambda Calculus with Abbreviations") +
@@("documentation.html#bibtex" "BibTeX entry") ^ "."
* }
]
- [ { name "ldp3" "<span class=\"date\">R2.</span>" "" } {
+ [ { name "ldR2" "<span class=\"date\">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") +
@@("documentation.html#bibtex" "BibTeX entry") ^ "."
* }
]
- [ { name "ldp2" "<span class=\"date\">R1.</span>" "" } {
+ [ { name "ldR1" "<span class=\"date\">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") +
@@("documentation.html#bibtex" "BibTeX entry") ^ "."
* }
]
- [ { name "ldt5" "<span class=\"date\">P5.</span>" "" } {
+ [ { name "ldP5" "<span class=\"date\">P5.</span>" "" } {
"F. Guidi:" +
@@("download/ld_talk_5s.pdf" "The Formal System λδ") +
"(<span class=\"date\">2008-10</span>)." +
"Presentation at Advances in Constructive Topology and Logical Foundations (slides)."
* }
]
- [ { name "ldt4" "<span class=\"date\">P4.</span>" "" } {
+ [ { name "ldP4" "<span class=\"date\">P4.</span>" "" } {
"F. Guidi:" +
@@("download/ld_talk_4s.pdf"
"Towards the Unification of Terms, Types and Contexts") +
"Presentation at Types 2008 (slides)."
* }
]
- [ { name "ldt3" "<span class=\"date\">P3.</span>" "" } {
+ [ { name "ldP3" "<span class=\"date\">P3.</span>" "" } {
"F. Guidi:" +
@@("download/ld_talk_3s.pdf"
"Lambda Types on the Lambda Calculus with Abbreviations") +
"Presentation at CiE 2007 (slides)."
* }
]
- [ { name "ldt2" "<span class=\"date\">P2.</span>" "" } {
+ [ { name "ldP2" "<span class=\"date\">P2.</span>" "" } {
"F. Guidi:" +
@@("download/ld_talk_2s.pdf"
"Lambda Tipi sul Lambda Calcolo con Abbreviazioni") +
"<span class=\"date\">in Italian</span>)."
* }
]
- [ { name "ldt1" "<span class=\"date\">P1.</span>" "" } {
+ [ { name "ldP1" "<span class=\"date\">P1.</span>" "" } {
"F. Guidi:" +
@@("download/ld_talk_1s.pdf"
"Lambda Tipi sul Lambda Calcolo con Abbreviazioni: una Specifica Certificata") +
name "documentation_2"
table {
- [ { name "ldp7" "<span class=\"date\">R5.</span>" "" } {
+ [ { name "ldR5" "<span class=\"date\">R5.</span>" "" } {
"F. Guidi:" +
@@("download/cie_2010.pdf"
"An Efficient Validation Procedure for the Formal System λδ") +
@@("documentation.html#bibtex" "BibTeX entry") ^ "."
* }
]
- [ { name "ldp6" "<span class=\"date\">R4.</span>" "" } {
+ [ { name "ldR4" "<span class=\"date\">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") +
@@("documentation.html#bibtex" "BibTeX entry") ^ "."
* }
]
- [ { name "ldt8" "<span class=\"date\">P8.</span>" "" } {
+ [ { name "ldP8" "<span class=\"date\">P8.</span>" "" } {
"F. Guidi:" +
@@("download/ld_talk_8s.pdf"
"The Formal System λδ and the \"Three Problems\"") +
"Presentation at University of Bologna (slides)."
* }
]
- [ { name "ldt7" "<span class=\"date\">P7.</span>" "" } {
+ [ { name "ldP7" "<span class=\"date\">P7.</span>" "" } {
"F. Guidi:" +
@@("download/ld_talk_7s.pdf"
"An Efficient Validation Procedure for the Formal System λδ") +
"Presentation at CiE 2010 (slides)."
* }
]
- [ { name "ldt6" "<span class=\"date\">P6.</span>" "" } {
+ [ { name "ldP6" "<span class=\"date\">P6.</span>" "" } {
"F. Guidi:" +
@@("download/ld_talk_6s.pdf"
"A Validator for the Formal System λδ") +
Exploits a subset of "complete_rg" λδ as the intermediate language.
Features importation from ".hln" files containing λδ textual syntax.
The overall validation speed of the "Grundlagen der Analysis"
- increases of 22% with respect toversion 0.8.0.
+ increases of 22% with respect to version 0.8.0.
[Svn revision: 11032] (<rlink to="download/helena_0.8.1.tar.gz">archived source code</rlink>)
<list><item>
A <link to="http://www.jedsoft.org/jed/">Jed mode</link>
Supports "basic_rg" λδ with naive implementation of impredicative sort inclusion.
Features importation from <link to="http://www.win.tue.nl/automath/">Automath</link>
and exportation to <link to="http://www.w3.org/XML/">XML</link>.
- <rlink to="documentation.html#ldp6">Documentation</rlink>.
+ <rlink to="documentation.html#ldR4">Documentation (R4)</rlink>.
[Svn revision: 10304] (<rlink to="download/helena_0.8.0.tar.gz">archived source code</rlink>).
<list><item>
A <link to="http://www.jedsoft.org/jed/">Jed mode</link>
<sitemap name="sitemap"/>
<section5 name="milestones">Milestones</section5>
- <body>
- <news date="June 2014.">
- <rlink to="documentation.html#ldt8">First communication on λδ version 2.</rlink>
- </news>
- <news date="December 2012.">
- The character "_" is removed from the denomination "lambda_delta":
- <list>
- <item>
- The denomination "\lambda\delta" is used in λδ-related texts.
- </item>
- <item>
- The denomination "lambdadelta" is used in λδ-related identifiers.
- </item>
- <item>
- Permanent λδ URL acquired:
- <rlink to="">http://lambdadelta.info/</rlink>
- (pointing at this site).
- </item>
- </list>
- </news>
- <news date="September 2011.">
- The denomination "lambda-delta" changes to "lambda_delta":
- <list>
- <item>
- The character "-" is reserved in λδ textual syntax
- (recognized by "Helena 0.8.1").
- </item>
- <item>
- Eventually, the occurrences of the character "-"
- will be replaced by "_" in all λδ-related identifiers.
- </item>
- <item>
- In particular, this refactoring involves file names and path names.
- </item>
- </list>
- </news>
- <news 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.">
- Transient λδ URL acquired: http://lambda-delta.info/ (expires on December 2012).
- </news>
- <news date="November 2010.">
- "Helena 0.8.1" is released.
- </news>
- <news 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.">
- "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.">
- This site is online.
- </news>
- <news date="July 2008.">
- <rlink to="documentation.html#ldp5">First journal paper on λδ</rlink>
- accepted for publication.
- </news>
- <news 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.">
- 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>
- <news date="March 2008.">
- The specification of λδ version 2 is started with Coq 7.3.1 (false start).
- </news>
- <news 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.">
- <rlink to="documentation.html#ldp3">λδ version 1</rlink>
- is released.
- </news>
- <news date="December 2005.">
- <rlink to="documentation.html#ldt1">First communication on λδ</rlink>.
- </news>
- <news date="May 2004.">
- The specification of <rlink to="version_1.html">λδ version 1</rlink>
- is started with Coq 7.3.1.
- </news>
- </body>
+
+ <news date="July 2014.">
+ A new version of this site is online.
+ </news>
+
+ <news date="June 2014.">
+ <rlink to="documentation.html#ldP8">First communication on λδ version 2.</rlink>
+ </news>
+
+ <news date="December 2012.">
+ The character "_" is removed from the denomination "lambda_delta":
+ <list><item>
+ The denomination "\lambda\delta" is used in λδ-related texts.
+ </item><item>
+ The denomination "lambdadelta" is used in λδ-related identifiers.
+ </item><item>
+ Permanent λδ URL acquired:
+ <rlink to="">http://lambdadelta.info/</rlink>
+ (pointing at this site).
+ </item></list>
+ </news>
+
+ <news date="September 2011.">
+ The denomination "lambda-delta" changes to "lambda_delta":
+ <list><item>
+ The character "-" is reserved in λδ textual syntax
+ (recognized by "Helena 0.8.1").
+ </item><item>
+ Eventually, the occurrences of the character "-"
+ will be replaced by "_" in all λδ-related identifiers.
+ </item><item>
+ In particular, this refactoring involves file names and path names.
+ </item></list>
+ </news>
+
+ <news 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.">
+ Transient λδ URL acquired: http://lambda-delta.info/ (expires on December 2012).
+ </news>
+
+ <news date="November 2010.">
+ "Helena 0.8.1" is released.
+ </news>
+
+ <news 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.">
+ "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.">
+ This site is online.
+ </news>
+
+ <news date="July 2008.">
+ <rlink to="documentation.html#ldJ1">First journal paper on λδ</rlink>
+ accepted for publication.
+ </news>
+
+ <news 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.">
+ 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>
+
+ <news date="March 2008.">
+ The specification of λδ version 2 is started with Coq 7.3.1 (false start).
+ </news>
+
+ <news 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.">
+ <rlink to="documentation.html#ldR2">λδ version 1</rlink>
+ is released.
+ </news>
+
+ <news date="December 2005.">
+ <rlink to="documentation.html#ldP1">First communication on λδ version 1</rlink>.
+ </news>
+
+ <news date="May 2004.">
+ The specification of <rlink to="version_1.html">λδ version 1</rlink>
+ is started with Coq 7.3.1.
+ </news>
<section4 name="visibility">Visibility</section4>
- <body>
- <news 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.">
- The <link to="http://www.yahoo.com/">Yahoo</link>
- search for "formal system lambda delta" gives
- 4 resources about λδ in the first 5 results.
- </news>
- </body>
+
+ <news 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.">
+ The <link to="http://www.yahoo.com/">Yahoo</link>
+ search for "formal system lambda delta" gives
+ 4 resources about λδ in the first 5 results.
+ </news>
<footer/>
</page>
}
class "green" {
[ @@"implementation"
- "(" ^ @@("implementation#specifications" "specifications") +
- @@("implementation#lddl" "library") +
+ "(" ^ @@("implementation#specifications" "specifications") + "-" +
+ @@("implementation#lddl" "library") + "-" +
@@("implementation#helena" "Helena") ^ ")"
* ]
[ @@("version_2" "Version 2")
- @@("ground_2" "Background") + @@("basic_2" "Core") + @@("apps_2" "Applications")
+ "(" ^ @@("ground_2" "Background") + "-" +
+ @@("basic_2" "Core") + "-" +
+ @@("apps_2" "Applications") ^ ")"
* ]
[ @@("version_1" "Version 1") * ] *
}
<sitemap name="sitemap"/>
<section6 name="foreword">Formats</section6>
+
<body>
The formal specification of λδ version 1
is available in the following formats:
- <topitem name="source">
- <rlink to="download/lambdadelta_1.tar.gz">lambdadelta_1 for Coq 7.3.1</rlink>
- (revised <date date="2012-10"/>).
- Source scripts.
- </topitem>
- <topitem name="static">
- <rlink to="static/matita/lambdadelta/">lambdadelta_1 for Matita 0.5"</rlink>
- (revised <date date="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">
- Confluence of reduction</rlink>
- (Church-Rosser property).
- </item>
- <item>
- <rlink to="static/matita/lambdadelta/basic_1/ty3/props/ty3_correct.con.html">
- Correctness of types</rlink>.
- </item>
- <item>
- <rlink to="static/matita/lambdadelta/basic_1/ty3/props/ty3_unique.con.html">
- Uniqueness of types up to conversion</rlink>.
- </item>
- <item>
- <rlink to="static/matita/lambdadelta/basic_1/ty3/pr3/ty3_sred_pr3.con.html">
- Subject reduction of the type assignment</rlink>.
- </item>
- <item>
- <rlink to="static/matita/lambdadelta/basic_1/ty3/arity_props/ty3_sn3.con.html">
- Strong normalization of the typed terms</rlink>.
- </item>
- <item>
- <rlink to="static/matita/lambdadelta/basic_1/ty3/dec/ty3_inference.con.html">
- Decidability of the type inference problem</rlink>.
- </item>
- </list>
- </topitem>
- <topitem name="dynamic">
- <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"/>).
- <link to="http://helm.cs.unibo.it/">HELM</link> directory.
- <date date="Notice: the HELM rendering engine is offline."/>
- </topitem>
</body>
+ <topitem name="source">
+ <rlink to="download/lambdadelta_1.tar.gz">lambdadelta_1 for Coq 7.3.1</rlink>
+ (revised <date date="2012-10"/>).
+ Source scripts.
+ </topitem>
+
+ <topitem name="static">
+ <rlink to="static/matita/lambdadelta/">lambdadelta_1 for Matita 0.5"</rlink>
+ (revised <date date="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">
+ Confluence of reduction</rlink>
+ (Church-Rosser property).
+ </item><item>
+ <rlink to="static/matita/lambdadelta/basic_1/ty3/props/ty3_correct.con.html">
+ Correctness of types</rlink>.
+ </item><item>
+ <rlink to="static/matita/lambdadelta/basic_1/ty3/props/ty3_unique.con.html">
+ Uniqueness of types up to conversion</rlink>.
+ </item><item>
+ <rlink to="static/matita/lambdadelta/basic_1/ty3/pr3/ty3_sred_pr3.con.html">
+ Subject reduction of the type assignment</rlink>.
+ </item><item>
+ <rlink to="static/matita/lambdadelta/basic_1/ty3/arity_props/ty3_sn3.con.html">
+ Strong normalization of the typed terms</rlink>.
+ </item><item>
+ <rlink to="static/matita/lambdadelta/basic_1/ty3/dec/ty3_inference.con.html">
+ Decidability of the type inference problem</rlink>.
+ </item></list>
+ </topitem>
+
+ <topitem name="dynamic">
+ <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"/>).
+ <link to="http://helm.cs.unibo.it/">HELM</link> directory.
+ <date date="Notice: the HELM rendering engine is offline."/>
+ </topitem>
+
<footer/>
</page>
<sitemap name="sitemap"/>
<section4 name="foreword">Formats</section4>
+
<body>
The formal specification of λδ version 2
is available in the following formats:
- <topitem name="source">
- <rlink to="download/lambdadelta_2.tar.gz">lambdadelta_2 for Matita 0.99.2</rlink>
- (revised <date date="2014-07"/>).
- Source scripts.
- </topitem>
- <topitem name="parts">
- <rlink to="ground_2.html">Background</rlink>,
- <rlink to="basic_2.html">Core</rlink>,
- <rlink to="apps_2.html">Applications</rlink>.
- Informational pages on the parts of the specification.
- </topitem>
</body>
+ <topitem name="source">
+ <rlink to="download/lambdadelta_2.tar.gz">lambdadelta_2 for Matita 0.99.2</rlink>
+ (revised <date date="2014-07"/>).
+ Source scripts.
+ </topitem>
+
+ <topitem name="parts">
+ <rlink to="ground_2.html">Background</rlink>,
+ <rlink to="basic_2.html">Core</rlink>,
+ <rlink to="apps_2.html">Applications</rlink>.
+ Informational pages on the parts of the specification.
+ </topitem>
+
<footer/>
</page>
projects / helm.git / commitdiff