<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 21 Jul 2016 16:50:49 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:08:42 +0200</div>
</body>
</html>
<tbody>
<tr>
<td class="snns capitalize italic sky">
- <a href="http://lambdadelta.info/index.html">home</a>
+ <a href="http://lambdadelta.info/home.html">home</a>
</td>
<td class="snns capitalize italic magenta">
<a href="http://lambdadelta.info/news.html">news</a>
</tr>
<tr>
<td class="snns capitalize sky">
- <a href="http://lambdadelta.info/index.html#foreword">foreword</a>
+ <a href="http://lambdadelta.info/home.html#foreword">foreword</a>
</td>
<td class="snns capitalize magenta">
<a href="http://lambdadelta.info/news.html#milestones">milestones</a>
<a href="http://lambdadelta.info/implementation.html#helena">helena</a>
</td>
<td class="ssnn capitalize green">
- <br />
+ <a href="http://lambdadelta.info/osn/">Open Symbolic Notation (OSN)</a>
</td>
</tr>
<tr>
<td class="snss capitalize sky">
- <a href="http://lambdadelta.info/index.html#citations">citations</a>
+ <a href="http://lambdadelta.info/home.html#citations">citations</a>
</td>
<td class="snss capitalize magenta">
<a href="http://lambdadelta.info/news.html#visibility">visibility</a>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 21 Jul 2016 16:50:49 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:08:42 +0200</div>
</body>
</html>
<tbody>
<tr>
<td class="snns capitalize italic sky">
- <a href="http://lambdadelta.info/index.html">home</a>
+ <a href="http://lambdadelta.info/home.html">home</a>
</td>
<td class="snns capitalize italic magenta">
<a href="http://lambdadelta.info/news.html">news</a>
</tr>
<tr>
<td class="snns capitalize sky">
- <a href="http://lambdadelta.info/index.html#foreword">foreword</a>
+ <a href="http://lambdadelta.info/home.html#foreword">foreword</a>
</td>
<td class="snns capitalize magenta">
<a href="http://lambdadelta.info/news.html#milestones">milestones</a>
<a href="http://lambdadelta.info/implementation.html#helena">helena</a>
</td>
<td class="ssnn capitalize green">
- <br />
+ <a href="http://lambdadelta.info/osn/">Open Symbolic Notation (OSN)</a>
</td>
</tr>
<tr>
<td class="snss capitalize sky">
- <a href="http://lambdadelta.info/index.html#citations">citations</a>
+ <a href="http://lambdadelta.info/home.html#citations">citations</a>
</td>
<td class="snss capitalize magenta">
<a href="http://lambdadelta.info/news.html#visibility">visibility</a>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 21 Jul 2016 16:50:49 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:08:42 +0200</div>
</body>
</html>
<tbody>
<tr>
<td class="snns capitalize italic sky">
- <a href="http://lambdadelta.info/index.html">home</a>
+ <a href="http://lambdadelta.info/home.html">home</a>
</td>
<td class="snns capitalize italic magenta">
<a href="http://lambdadelta.info/news.html">news</a>
</tr>
<tr>
<td class="snns capitalize sky">
- <a href="http://lambdadelta.info/index.html#foreword">foreword</a>
+ <a href="http://lambdadelta.info/home.html#foreword">foreword</a>
</td>
<td class="snns capitalize magenta">
<a href="http://lambdadelta.info/news.html#milestones">milestones</a>
<a href="http://lambdadelta.info/implementation.html#helena">helena</a>
</td>
<td class="ssnn capitalize green">
- <br />
+ <a href="http://lambdadelta.info/osn/">Open Symbolic Notation (OSN)</a>
</td>
</tr>
<tr>
<td class="snss capitalize sky">
- <a href="http://lambdadelta.info/index.html#citations">citations</a>
+ <a href="http://lambdadelta.info/home.html#citations">citations</a>
</td>
<td class="snss capitalize magenta">
<a href="http://lambdadelta.info/news.html#visibility">visibility</a>
<tr>
<td class="snns capitalize italic cyan">sizes</td>
<td class="snns italic cyan">files</td>
- <td class="snnn right italic cyan">154</td>
+ <td class="snnn right italic cyan">150</td>
<td class="snns italic cyan">characters</td>
- <td class="snnn right italic cyan">136477</td>
+ <td class="snnn right italic cyan">128505</td>
<td class="snns italic cyan">nodes</td>
- <td class="ssnn right italic cyan">748562</td>
+ <td class="ssnn right italic cyan">646562</td>
</tr>
<tr>
<td class="snns capitalize italic green">propositions</td>
<td class="snns italic green">theorems</td>
<td class="snnn right italic green">45</td>
<td class="snns italic green">lemmas</td>
- <td class="snnn right italic green">500</td>
+ <td class="snnn right italic green">476</td>
<td class="snns italic green">total</td>
- <td class="ssnn right italic green">545</td>
+ <td class="ssnn right italic green">521</td>
</tr>
<tr>
<td class="snss capitalize italic yellow">concepts</td>
<td class="snss italic yellow">declared</td>
<td class="snsn right italic yellow">23</td>
<td class="snss italic yellow">defined</td>
- <td class="snsn right italic yellow">38</td>
+ <td class="snsn right italic yellow">37</td>
<td class="snss italic yellow">total</td>
- <td class="sssn right italic yellow">61</td>
+ <td class="sssn right italic yellow">60</td>
</tr>
</tbody>
</table>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 21 Jul 2016 16:50:49 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:08:42 +0200</div>
</body>
</html>
<tbody>
<tr>
<td class="snns capitalize italic sky">
- <a href="http://lambdadelta.info/index.html">home</a>
+ <a href="http://lambdadelta.info/home.html">home</a>
</td>
<td class="snns capitalize italic magenta">
<a href="http://lambdadelta.info/news.html">news</a>
</tr>
<tr>
<td class="snns capitalize sky">
- <a href="http://lambdadelta.info/index.html#foreword">foreword</a>
+ <a href="http://lambdadelta.info/home.html#foreword">foreword</a>
</td>
<td class="snns capitalize magenta">
<a href="http://lambdadelta.info/news.html#milestones">milestones</a>
<a href="http://lambdadelta.info/implementation.html#helena">helena</a>
</td>
<td class="ssnn capitalize green">
- <br />
+ <a href="http://lambdadelta.info/osn/">Open Symbolic Notation (OSN)</a>
</td>
</tr>
<tr>
<td class="snss capitalize sky">
- <a href="http://lambdadelta.info/index.html#citations">citations</a>
+ <a href="http://lambdadelta.info/home.html#citations">citations</a>
</td>
<td class="snss capitalize magenta">
<a href="http://lambdadelta.info/news.html#visibility">visibility</a>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 21 Jul 2016 16:50:48 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:08:42 +0200</div>
</body>
</html>
<tbody>
<tr>
<td class="snns capitalize italic sky">
- <a href="http://lambdadelta.info/index.html">home</a>
+ <a href="http://lambdadelta.info/home.html">home</a>
</td>
<td class="snns capitalize italic magenta">
<a href="http://lambdadelta.info/news.html">news</a>
</tr>
<tr>
<td class="snns capitalize sky">
- <a href="http://lambdadelta.info/index.html#foreword">foreword</a>
+ <a href="http://lambdadelta.info/home.html#foreword">foreword</a>
</td>
<td class="snns capitalize magenta">
<a href="http://lambdadelta.info/news.html#milestones">milestones</a>
<a href="http://lambdadelta.info/implementation.html#helena">helena</a>
</td>
<td class="ssnn capitalize green">
- <br />
+ <a href="http://lambdadelta.info/osn/">Open Symbolic Notation (OSN)</a>
</td>
</tr>
<tr>
<td class="snss capitalize sky">
- <a href="http://lambdadelta.info/index.html#citations">citations</a>
+ <a href="http://lambdadelta.info/home.html#citations">citations</a>
</td>
<td class="snss capitalize magenta">
<a href="http://lambdadelta.info/news.html#visibility">visibility</a>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 21 Jul 2016 16:50:49 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:08:42 +0200</div>
</body>
</html>
<tbody>
<tr>
<td class="snns capitalize italic sky">
- <a href="http://lambdadelta.info/index.html">home</a>
+ <a href="http://lambdadelta.info/home.html">home</a>
</td>
<td class="snns capitalize italic magenta">
<a href="http://lambdadelta.info/news.html">news</a>
</tr>
<tr>
<td class="snns capitalize sky">
- <a href="http://lambdadelta.info/index.html#foreword">foreword</a>
+ <a href="http://lambdadelta.info/home.html#foreword">foreword</a>
</td>
<td class="snns capitalize magenta">
<a href="http://lambdadelta.info/news.html#milestones">milestones</a>
<a href="http://lambdadelta.info/implementation.html#helena">helena</a>
</td>
<td class="ssnn capitalize green">
- <br />
+ <a href="http://lambdadelta.info/osn/">Open Symbolic Notation (OSN)</a>
</td>
</tr>
<tr>
<td class="snss capitalize sky">
- <a href="http://lambdadelta.info/index.html#citations">citations</a>
+ <a href="http://lambdadelta.info/home.html#citations">citations</a>
</td>
<td class="snss capitalize magenta">
<a href="http://lambdadelta.info/news.html#visibility">visibility</a>
<tr>
<td class="snns capitalize italic cyan">sizes</td>
<td class="snns italic cyan">files</td>
- <td class="snnn right italic cyan">94</td>
+ <td class="snnn right italic cyan">92</td>
<td class="snns italic cyan">characters</td>
- <td class="snnn right italic cyan">129419</td>
+ <td class="snnn right italic cyan">125262</td>
<td class="snns italic cyan">nodes</td>
- <td class="ssnn right italic cyan">291484</td>
+ <td class="ssnn right italic cyan">265747</td>
</tr>
<tr>
<td class="snns capitalize italic green">propositions</td>
<td class="snns italic green">theorems</td>
- <td class="snnn right italic green">35</td>
+ <td class="snnn right italic green">33</td>
<td class="snns italic green">lemmas</td>
- <td class="snnn right italic green">610</td>
+ <td class="snnn right italic green">588</td>
<td class="snns italic green">total</td>
- <td class="ssnn right italic green">645</td>
+ <td class="ssnn right italic green">621</td>
</tr>
<tr>
<td class="snss capitalize italic yellow">concepts</td>
<td class="snss italic yellow">declared</td>
- <td class="snsn right italic yellow">61</td>
+ <td class="snsn right italic yellow">60</td>
<td class="snss italic yellow">defined</td>
- <td class="snsn right italic yellow">64</td>
+ <td class="snsn right italic yellow">63</td>
<td class="snss italic yellow">total</td>
- <td class="sssn right italic yellow">125</td>
+ <td class="sssn right italic yellow">123</td>
</tr>
</tbody>
</table>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 21 Jul 2016 16:50:49 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:08:42 +0200</div>
</body>
</html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN" "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml" dir="ltr" lang="en-us">
+ <head>
+ <meta http-equiv="Content-Language" content="en-us" />
+ <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 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" />
+ <link rel="shortcut icon" href="http://lambdadelta.info/images/crux_16.ico" />
+ </head>
+ <body lang="en-US">
+ <div class="spacer">
+ <a href="http://lambdadelta.info/">
+ <img class="icon32" alt="[\lambda\delta home]" title="\lambda\delta home" src="http://lambdadelta.info/images/crux_32.png" />
+ </a>
+ </div>
+ <div class="head1">The Formal Systems of the λδ (\lambda\delta) Family</div>
+ <div class="spacer">
+ <img class="rule" alt="[Spacer]" title="\lambda\delta 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/home.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 white">
+ <a href="http://lambdadelta.info/specification.html">specification</a>
+ </td>
+ <td class="snnn capitalize italic white">
+ <br />
+ </td>
+ <td class="snnn capitalize italic white">
+ <br />
+ </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/implementation.html">implementation</a>
+ </td>
+ <td class="ssnn capitalize italic green">
+ <br />
+ </td>
+ </tr>
+ <tr>
+ <td class="snns capitalize sky">
+ <a href="http://lambdadelta.info/home.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 white">
+ <a href="http://lambdadelta.info/specification.html#v2">version 2</a>
+ </td>
+ <td class="snnn capitalize white">(<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="snnn capitalize white">
+ <br />
+ </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/implementation.html#helena">helena</a>
+ </td>
+ <td class="ssnn capitalize green">
+ <a href="http://lambdadelta.info/osn/">Open Symbolic Notation (OSN)</a>
+ </td>
+ </tr>
+ <tr>
+ <td class="snss capitalize sky">
+ <a href="http://lambdadelta.info/home.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 white">
+ <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
+ </td>
+ <td class="snsn capitalize white">(<a href="http://lambdadelta.info/ground_1.html">background</a> - <a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
+ <td class="snsn capitalize white">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</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/implementation.html#lddl">library</a>
+ </td>
+ <td class="sssn capitalize green">(<a href="http://lambdadelta.info/static/lddl/">static LDDL directory</a>)</td>
+ </tr>
+ </tbody>
+ </table>
+ </div>
+ <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="foreword">Foreword <img class="icon37" alt="[butterfly]" title="\lambda\delta butterfly" src="http://lambdadelta.info/images/b9.png" />
+ </div>
+ <div xmlns:ld="http://lambdadelta.info/" class="text">
+ The formal systems of the λδ (\lambda\delta) family are typed λ-calculi aiming to support
+ the foundational frameworks for Mathematics that require an underlying specification language
+ (for example the <a href="http://www.math.unipd.it/~maietti/">Minimalist Foundation</a>
+ and its predecessors).
+ </div>
+ <div xmlns:ld="http://lambdadelta.info/" class="text">
+ The λδ family is developed within the
+ <a href="http://helm.cs.unibo.it/">Hypertextual Electronic Library of Mathematics</a>
+ as a set of machine-checked digital specifications.
+ </div>
+ <div xmlns:ld="http://lambdadelta.info/" class="text">
+ This is the family logo: <a href="http://lambdadelta.info/images/crux_177.png">crux_177.png</a>
+ (revised <span class="emph alpha">2012-09</span>).
+ </div>
+ <div xmlns:ld="http://lambdadelta.info/" class="text">
+ <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).
+ To change the current font follow:
+ "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="[butterfly]" title="\lambda\delta butterfly" src="http://lambdadelta.info/images/b9.png" />
+ </div>
+ <div xmlns:ld="http://lambdadelta.info/" class="text">
+ This is a list of publications citing λδ documentation.
+ </div>
+ <ul xmlns:ld="http://lambdadelta.info/" id="C7">
+ <li>
+ C. Dunchev, F. Guidi, C. Sacerdoti Coen, E. Tassi:
+ <span class="emph alpha">ELPI: Fast, Embeddable, λProlog Interpreter</span>
+ (2015). In proc. of LPAR 20. Lecture Notes in Computer Science, 9450, pp. 460-468. Springer.
+ </li>
+ </ul>
+ <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 Journal of Automated Reasoning, 49(3), pp. 427-451. Springer.
+ </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). Technical report.
+ </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 Annals of Pure and Applied Logic, 160(3), pp. 319-354. Elsevier.
+ </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). Technical report.
+ </li>
+ </ul>
+ <!-- ===================================================================== -->
+ <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="disclaimer">Disclaimer <img class="icon37" alt="[butterfly]" title="\lambda\delta butterfly" src="http://lambdadelta.info/images/b9.png" />
+ </div>
+ <div xmlns:ld="http://lambdadelta.info/" class="text">
+ The systems of the λδ family <span class="emph alpha">are not</span> related intentionally to
+ any other system having (variations of) the symbols λ and δ in its name or syntax.
+ Examples include (but are not limited to):
+ </div>
+ <ul xmlns:ld="http://lambdadelta.info/" id="D1">
+ <li>
+ <span class="emph alpha">λ-δ</span> of
+ A. Church:
+ <span class="emph alpha">The calculi of lambda-conversion</span>
+ (1941).
+ Annals of Mathematics Studies 6.
+ Princeton University Press.
+ </li>
+ </ul>
+ <ul xmlns:ld="http://lambdadelta.info/" id="D2">
+ <li>
+ <span class="emph alpha">∆Λ</span> of
+ N.G. de Bruijn:
+ <span class="emph alpha">Generalizing Automath by means of a lambda-typed lambda calculus</span>
+ (1987).
+ In Lecture Notes in Pure and Applied Mathematics 106, pp. 71-92.
+ Marcel Dekker.
+ </li>
+ </ul>
+ <ul xmlns:ld="http://lambdadelta.info/" id="D3">
+ <li>
+ <span class="emph alpha">λ<sub>∆</sub>
+ </span> of
+ N.J. Rehof, M.H. Sørensen:
+ <span class="emph alpha">The λ<sub>∆</sub>-calculus</span>
+ (1994).
+ In Lecture Notes in Computer Science, 789, pp. 516–542.
+ Springer.
+ </li>
+ </ul>
+ <ul xmlns:ld="http://lambdadelta.info/" id="D4">
+ <li>
+ <span class="emph alpha">λ∆</span> of
+ S. Ronchi Della Rocca, L. Paolini:
+ <span class="emph alpha">The Parametric Lambda Calculus</span>
+ (2004).
+ Texts in Theoretical Computer Science, An EATCS Series.
+ Springer.
+ </li>
+ </ul>
+ <ul xmlns:ld="http://lambdadelta.info/" id="D5">
+ <li>
+ <span class="emph alpha">λD</span> of
+ R. Nederpelt, H. Geuvers:
+ <span class="emph alpha">Type Theory and Formal Proof</span>
+ (2014).
+ Cambridge University Press.
+ </li>
+ </ul>
+ <ul xmlns:ld="http://lambdadelta.info/" id="D6">
+ <li>
+ <span class="emph alpha">Cλξ</span> of
+ N.G. de Bruijn:
+ <span class="emph alpha">A namefree lambda calculus with facilities for internal definition of expressions and segments</span>
+ (1978).
+ TH-report 78-WSK-03.
+ Eindhoven University of Technology, Eindhoven.
+ </li>
+ </ul>
+ <div xmlns:ld="http://lambdadelta.info/" class="text">
+ <img class="icon32" alt="[Smiling face]" title="Smile!" src="http://lambdadelta.info/images/smile.png" />
+ Moreover, the systems of the λδ family <span class="emph alpha">are not</span> related intentionally to
+ <a href="http://umineko.wikia.com/wiki/Lambdadelta">Lady Lambdadelta</a>,
+ the Witch of Certainty of the sound novel
+ <a href="https://it.wikipedia.org/wiki/Umineko_no_naku_koro_ni">Umineko no Naku Koro ni</a>.
+ </div>
+ <div class="spacer">
+ <img class="rule" alt="[Spacer]" title="\lambda\delta 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">
+ <a href="http://validator.w3.org/check?uri=referer">
+ <img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue" />
+ </a>
+ <a href="http://jigsaw.w3.org/css-validator/check/referer">
+ <img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue" />
+ </a>
+ <a href="http://www.w3.org/XML/">
+ <img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambdadelta.info/images/xml_xsl2.png" />
+ </a>
+ <a href="http://www.w3.org/Graphics/PNG/">
+ <img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambdadelta.info/images/PNGnow2.png" />
+ </a>
+ <a href="http://www.anybrowser.org/campaign/">
+ <img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png" />
+ </a>
+ </div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">
+ <br />
+ </div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:08:41 +0200</div>
+ </body>
+</html>
<tbody>
<tr>
<td class="snns capitalize italic sky">
- <a href="http://lambdadelta.info/index.html">home</a>
+ <a href="http://lambdadelta.info/home.html">home</a>
</td>
<td class="snns capitalize italic magenta">
<a href="http://lambdadelta.info/news.html">news</a>
</tr>
<tr>
<td class="snns capitalize sky">
- <a href="http://lambdadelta.info/index.html#foreword">foreword</a>
+ <a href="http://lambdadelta.info/home.html#foreword">foreword</a>
</td>
<td class="snns capitalize magenta">
<a href="http://lambdadelta.info/news.html#milestones">milestones</a>
<a href="http://lambdadelta.info/implementation.html#helena">helena</a>
</td>
<td class="ssnn capitalize green">
- <br />
+ <a href="http://lambdadelta.info/osn/">Open Symbolic Notation (OSN)</a>
</td>
</tr>
<tr>
<td class="snss capitalize sky">
- <a href="http://lambdadelta.info/index.html#citations">citations</a>
+ <a href="http://lambdadelta.info/home.html#citations">citations</a>
</td>
<td class="snss capitalize magenta">
<a href="http://lambdadelta.info/news.html#visibility">visibility</a>
<div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="tools">Tools <img class="icon37" alt="[butterfly]" title="\lambda\delta butterfly" src="http://lambdadelta.info/images/b5.png" />
</div>
<div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="osn">
- <a href="http://lambdadelta.info/osn.html">
+ <a href="http://lambdadelta.info/osn/">
<img class="w3c" alt="[Open Symbolic Notation logo]" title="OSN: Open Symbolic Notation" src="http://lambdadelta.info/images/osn_label.png" />
</a> Open Symbolic Notation</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
Open Symbolic Notation, abbreviated OSN,
is an easy and flexible data-interchange text format
intended for the lightweight representation of
- generic abstract syntax trees in the domain of formal systems.
- Additional information will appear soon.
+ generic abstract syntax trees in the domain of formal languages.
+ Additional information is available at <a href="http://lambdadelta.info/osn/">OSN web site</a>.
</div>
<div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="helena">
<img class="icon32" alt="[Helena logo]" title="Helena" src="http://lambdadelta.info/images/helena_32.png" /> Helena</div>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 21 Jul 2016 16:50:48 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:08:42 +0200</div>
</body>
</html>
+++ /dev/null
-<?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN" "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
-<html xmlns="http://www.w3.org/1999/xhtml" dir="ltr" lang="en-us">
- <head>
- <meta http-equiv="Content-Language" content="en-us" />
- <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 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" />
- <link rel="shortcut icon" href="http://lambdadelta.info/images/crux_16.ico" />
- </head>
- <body lang="en-US">
- <div class="spacer">
- <a href="http://lambdadelta.info/">
- <img class="icon32" alt="[\lambda\delta home]" title="\lambda\delta home" src="http://lambdadelta.info/images/crux_32.png" />
- </a>
- </div>
- <div class="head1">The Formal Systems of the λδ (\lambda\delta) Family</div>
- <div class="spacer">
- <img class="rule" alt="[Spacer]" title="\lambda\delta 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 white">
- <a href="http://lambdadelta.info/specification.html">specification</a>
- </td>
- <td class="snnn capitalize italic white">
- <br />
- </td>
- <td class="snnn capitalize italic white">
- <br />
- </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/implementation.html">implementation</a>
- </td>
- <td class="ssnn capitalize italic green">
- <br />
- </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 white">
- <a href="http://lambdadelta.info/specification.html#v2">version 2</a>
- </td>
- <td class="snnn capitalize white">(<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="snnn capitalize white">
- <br />
- </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/implementation.html#helena">helena</a>
- </td>
- <td class="ssnn capitalize green">
- <br />
- </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 white">
- <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
- </td>
- <td class="snsn capitalize white">(<a href="http://lambdadelta.info/ground_1.html">background</a> - <a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
- <td class="snsn capitalize white">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</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/implementation.html#lddl">library</a>
- </td>
- <td class="sssn capitalize green">(<a href="http://lambdadelta.info/static/lddl/">static LDDL directory</a>)</td>
- </tr>
- </tbody>
- </table>
- </div>
- <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="foreword">Foreword <img class="icon37" alt="[butterfly]" title="\lambda\delta butterfly" src="http://lambdadelta.info/images/b9.png" />
- </div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
- The formal systems of the λδ (\lambda\delta) family are typed λ-calculi aiming to support
- the foundational frameworks for Mathematics that require an underlying specification language
- (for example the <a href="http://www.math.unipd.it/~maietti/">Minimalist Foundation</a>
- and its predecessors).
- </div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
- The λδ family is developed within the
- <a href="http://helm.cs.unibo.it/">Hypertextual Electronic Library of Mathematics</a>
- as a set of machine-checked digital specifications.
- </div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
- This is the family logo: <a href="http://lambdadelta.info/images/crux_177.png">crux_177.png</a>
- (revised <span class="emph alpha">2012-09</span>).
- </div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
- <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).
- To change the current font follow:
- "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="[butterfly]" title="\lambda\delta butterfly" src="http://lambdadelta.info/images/b9.png" />
- </div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
- This is a list of publications citing λδ documentation.
- </div>
- <ul xmlns:ld="http://lambdadelta.info/" id="C7">
- <li>
- C. Dunchev, F. Guidi, C. Sacerdoti Coen, E. Tassi:
- <span class="emph alpha">ELPI: Fast, Embeddable, λProlog Interpreter</span>
- (2015). In proc. of LPAR 20. Lecture Notes in Computer Science, 9450, pp. 460-468. Springer.
- </li>
- </ul>
- <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 Journal of Automated Reasoning, 49(3), pp. 427-451. Springer.
- </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). Technical report.
- </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 Annals of Pure and Applied Logic, 160(3), pp. 319-354. Elsevier.
- </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). Technical report.
- </li>
- </ul>
- <!-- ===================================================================== -->
- <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="disclaimer">Disclaimer <img class="icon37" alt="[butterfly]" title="\lambda\delta butterfly" src="http://lambdadelta.info/images/b9.png" />
- </div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
- The systems of the λδ family <span class="emph alpha">are not</span> related intentionally to
- any other system having (variations of) the symbols λ and δ in its name or syntax.
- Examples include (but are not limited to):
- </div>
- <ul xmlns:ld="http://lambdadelta.info/" id="D1">
- <li>
- <span class="emph alpha">λ-δ</span> of
- A. Church:
- <span class="emph alpha">The calculi of lambda-conversion</span>
- (1941).
- Annals of Mathematics Studies 6.
- Princeton University Press.
- </li>
- </ul>
- <ul xmlns:ld="http://lambdadelta.info/" id="D2">
- <li>
- <span class="emph alpha">∆Λ</span> of
- N.G. de Bruijn:
- <span class="emph alpha">Generalizing Automath by means of a lambda-typed lambda calculus</span>
- (1987).
- In Lecture Notes in Pure and Applied Mathematics 106, pp. 71-92.
- Marcel Dekker.
- </li>
- </ul>
- <ul xmlns:ld="http://lambdadelta.info/" id="D3">
- <li>
- <span class="emph alpha">λ<sub>∆</sub>
- </span> of
- N.J. Rehof, M.H. Sørensen:
- <span class="emph alpha">The λ<sub>∆</sub>-calculus</span>
- (1994).
- In Lecture Notes in Computer Science, 789, pp. 516–542.
- Springer.
- </li>
- </ul>
- <ul xmlns:ld="http://lambdadelta.info/" id="D4">
- <li>
- <span class="emph alpha">λ∆</span> of
- S. Ronchi Della Rocca, L. Paolini:
- <span class="emph alpha">The Parametric Lambda Calculus</span>
- (2004).
- Texts in Theoretical Computer Science, An EATCS Series.
- Springer.
- </li>
- </ul>
- <ul xmlns:ld="http://lambdadelta.info/" id="D5">
- <li>
- <span class="emph alpha">λD</span> of
- R. Nederpelt, H. Geuvers:
- <span class="emph alpha">Type Theory and Formal Proof</span>
- (2014).
- Cambridge University Press.
- </li>
- </ul>
- <ul xmlns:ld="http://lambdadelta.info/" id="D6">
- <li>
- <span class="emph alpha">Cλξ</span> of
- N.G. de Bruijn:
- <span class="emph alpha">A namefree lambda calculus with facilities for internal definition of expressions and segments</span>
- (1978).
- TH-report 78-WSK-03.
- Eindhoven University of Technology, Eindhoven.
- </li>
- </ul>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
- <img class="icon32" alt="[Smiling face]" title="Smile!" src="http://lambdadelta.info/images/smile.png" />
- Moreover, the systems of the λδ family <span class="emph alpha">are not</span> related intentionally to
- <a href="http://umineko.wikia.com/wiki/Lambdadelta">Lady Lambdadelta</a>,
- the Witch of Certainty of the sound novel
- <a href="https://it.wikipedia.org/wiki/Umineko_no_naku_koro_ni">Umineko no Naku Koro ni</a>.
- </div>
- <div class="spacer">
- <img class="rule" alt="[Spacer]" title="\lambda\delta 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">
- <a href="http://validator.w3.org/check?uri=referer">
- <img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue" />
- </a>
- <a href="http://jigsaw.w3.org/css-validator/check/referer">
- <img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue" />
- </a>
- <a href="http://www.w3.org/XML/">
- <img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambdadelta.info/images/xml_xsl2.png" />
- </a>
- <a href="http://www.w3.org/Graphics/PNG/">
- <img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambdadelta.info/images/PNGnow2.png" />
- </a>
- <a href="http://www.anybrowser.org/campaign/">
- <img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png" />
- </a>
- </div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">
- <br />
- </div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 21 Jul 2016 16:50:48 +0200</div>
- </body>
-</html>
<tbody>
<tr>
<td class="snns capitalize italic sky">
- <a href="http://lambdadelta.info/index.html">home</a>
+ <a href="http://lambdadelta.info/home.html">home</a>
</td>
<td class="snns capitalize italic magenta">
<a href="http://lambdadelta.info/news.html">news</a>
</tr>
<tr>
<td class="snns capitalize sky">
- <a href="http://lambdadelta.info/index.html#foreword">foreword</a>
+ <a href="http://lambdadelta.info/home.html#foreword">foreword</a>
</td>
<td class="snns capitalize magenta">
<a href="http://lambdadelta.info/news.html#milestones">milestones</a>
<a href="http://lambdadelta.info/implementation.html#helena">helena</a>
</td>
<td class="ssnn capitalize green">
- <br />
+ <a href="http://lambdadelta.info/osn/">Open Symbolic Notation (OSN)</a>
</td>
</tr>
<tr>
<td class="snss capitalize sky">
- <a href="http://lambdadelta.info/index.html#citations">citations</a>
+ <a href="http://lambdadelta.info/home.html#citations">citations</a>
</td>
<td class="snss capitalize magenta">
<a href="http://lambdadelta.info/news.html#visibility">visibility</a>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 21 Jul 2016 16:50:48 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:08:41 +0200</div>
</body>
</html>
</head>
<body lang="en-US">
<div class="spacer">
- <a href="http://lambdadelta.info/osn.html">
+ <a href="http://lambdadelta.info/osn/">
<img class="w3c" alt="[Open Symbolic Notation logo]" title="OSN: Open Symbolic Notation" src="http://lambdadelta.info/images/osn_label.png" />
</a>
</div>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 21 Jul 2016 16:50:49 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:08:41 +0200</div>
</body>
</html>
<tbody>
<tr>
<td class="snns capitalize italic sky">
- <a href="http://lambdadelta.info/index.html">home</a>
+ <a href="http://lambdadelta.info/home.html">home</a>
</td>
<td class="snns capitalize italic magenta">
<a href="http://lambdadelta.info/news.html">news</a>
</tr>
<tr>
<td class="snns capitalize sky">
- <a href="http://lambdadelta.info/index.html#foreword">foreword</a>
+ <a href="http://lambdadelta.info/home.html#foreword">foreword</a>
</td>
<td class="snns capitalize magenta">
<a href="http://lambdadelta.info/news.html#milestones">milestones</a>
<a href="http://lambdadelta.info/implementation.html#helena">helena</a>
</td>
<td class="ssnn capitalize green">
- <br />
+ <a href="http://lambdadelta.info/osn/">Open Symbolic Notation (OSN)</a>
</td>
</tr>
<tr>
<td class="snss capitalize sky">
- <a href="http://lambdadelta.info/index.html#citations">citations</a>
+ <a href="http://lambdadelta.info/home.html#citations">citations</a>
</td>
<td class="snss capitalize magenta">
<a href="http://lambdadelta.info/news.html#visibility">visibility</a>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 21 Jul 2016 16:50:49 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:08:42 +0200</div>
</body>
</html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<page xmlns="http://lambdadelta.info/"
+ description = "\lambda\delta home page"
+ title = "\lambda\delta home page"
+ logo = "crux"
+ head = "The Formal Systems of the λδ (\lambda\delta) Family"
+>
+ <sitemap name="sitemap"/>
+
+ <section9 name="foreword">Foreword</section9>
+ <body>
+ The formal systems of the λδ (\lambda\delta) family are typed λ-calculi aiming to support
+ the foundational frameworks for Mathematics that require an underlying specification language
+ (for example the <link to="http://www.math.unipd.it/~maietti/">Minimalist Foundation</link>
+ and its predecessors).
+ </body>
+ <body>
+ The λδ family is developed within the
+ <link to="http://helm.cs.unibo.it/">Hypertextual Electronic Library of Mathematics</link>
+ as a set of machine-checked digital specifications.
+ </body>
+ <body>
+ This is the family logo: <rlink to="images/crux_177.png">crux_177.png</rlink>
+ (revised <notice class="alpha" text="2012-09"/>).
+ </body>
+ <body>
+ <notice class="alpha" text="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).
+ To change the current font follow:
+ "Tools" menu → "Internet Options" entry → "General" tab → "Fonts" button.
+ </body>
+
+<!-- ===================================================================== -->
+
+ <section9 name="citations">Citations</section9>
+ <body>
+ This is a list of publications citing λδ documentation.
+ </body>
+
+ <topitem name="C7">
+ C. Dunchev, F. Guidi, C. Sacerdoti Coen, E. Tassi:
+ <notice class="alpha">ELPI: Fast, Embeddable, λProlog Interpreter</notice>
+ (2015). In proc. of LPAR 20. Lecture Notes in Computer Science, 9450, pp. 460-468. Springer.
+ </topitem>
+
+ <topitem name="C6">
+ A. Asperti, W. Ricciotti, C. Sacerdoti Coen, E. Tassi:
+ <notice class="alpha">Formal metatheory of programming languages in the Matita interactive theorem prover</notice>
+ (2012). In Journal of Automated Reasoning, 49(3), pp. 427-451. Springer.
+ </topitem>
+
+ <topitem name="C5">
+ M.E. Maietti:
+ <notice class="alpha">Consistency of the minimalist foundation with Church thesis and Bar Induction</notice>
+ (2012). Submitted article.
+ </topitem>
+
+ <topitem name="C4">
+ W. Ricciotti:
+ <notice class="alpha">Theoretical and implementation aspects in the mechanization of the metatheory of programming languages</notice>
+ (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">Faithful Reproductions of the Automath Landau Formalization</notice>
+ (2011). Technical report.
+ </topitem>
+
+ <topitem name="C2">
+ M.E. Maietti:
+ <notice class="alpha">A minimalist two-level foundation for constructive mathematics</notice>
+ (2009). In Annals of Pure and Applied Logic, 160(3), pp. 319-354. Elsevier.
+ </topitem>
+
+ <topitem name="C1">
+ V. Rahili:
+ <notice class="alpha">First Year Report: Realisability methods of proof and semantics with application to expansion</notice>
+ (July 2007). Technical report.
+ </topitem>
+
+<!-- ===================================================================== -->
+
+ <section9 name="disclaimer">Disclaimer</section9>
+ <body>
+ The systems of the λδ family <notice class="alpha" text="are not"/> related intentionally to
+ any other system having (variations of) the symbols λ and δ in its name or syntax.
+ Examples include (but are not limited to):
+ </body>
+
+ <topitem name="D1">
+ <notice class="alpha">λ-δ</notice> of
+ A. Church:
+ <notice class="alpha">The calculi of lambda-conversion</notice>
+ (1941).
+ Annals of Mathematics Studies 6.
+ Princeton University Press.
+ </topitem>
+
+ <topitem name="D2">
+ <notice class="alpha">∆Λ</notice> of
+ N.G. de Bruijn:
+ <notice class="alpha">Generalizing Automath by means of a lambda-typed lambda calculus</notice>
+ (1987).
+ In Lecture Notes in Pure and Applied Mathematics 106, pp. 71-92.
+ Marcel Dekker.
+ </topitem>
+
+ <topitem name="D3">
+ <notice class="alpha">λ<sub>∆</sub></notice> of
+ N.J. Rehof, M.H. Sørensen:
+ <notice class="alpha">The λ<sub>∆</sub>-calculus</notice>
+ (1994).
+ In Lecture Notes in Computer Science, 789, pp. 516–542.
+ Springer.
+ </topitem>
+
+ <topitem name="D4">
+ <notice class="alpha">λ∆</notice> of
+ S. Ronchi Della Rocca, L. Paolini:
+ <notice class="alpha">The Parametric Lambda Calculus</notice>
+ (2004).
+ Texts in Theoretical Computer Science, An EATCS Series.
+ Springer.
+ </topitem>
+
+ <topitem name="D5">
+ <notice class="alpha">λD</notice> of
+ R. Nederpelt, H. Geuvers:
+ <notice class="alpha">Type Theory and Formal Proof</notice>
+ (2014).
+ Cambridge University Press.
+ </topitem>
+
+ <topitem name="D6">
+ <notice class="alpha">Cλξ</notice> of
+ N.G. de Bruijn:
+ <notice class="alpha">A namefree lambda calculus with facilities for internal definition of expressions and segments</notice>
+ (1978).
+ TH-report 78-WSK-03.
+ Eindhoven University of Technology, Eindhoven.
+ </topitem>
+
+ <body>
+ <img logo="smile"/>
+ Moreover, the systems of the λδ family <notice class="alpha" text="are not"/> related intentionally to
+ <link to="http://umineko.wikia.com/wiki/Lambdadelta">Lady Lambdadelta</link>,
+ the Witch of Certainty of the sound novel
+ <link to="https://it.wikipedia.org/wiki/Umineko_no_naku_koro_ni">Umineko no Naku Koro ni</link>.
+ </body>
+
+ <footer/>
+</page>
Open Symbolic Notation, abbreviated OSN,
is an easy and flexible data-interchange text format
intended for the lightweight representation of
- generic abstract syntax trees in the domain of formal systems.
- Additional information will appear soon.
+ generic abstract syntax trees in the domain of formal languages.
+ Additional information is available at <rlink to="osn/">OSN web site</rlink>.
</body>
+++ /dev/null
-<?xml version="1.0" encoding="UTF-8"?>
-
-<page xmlns="http://lambdadelta.info/"
- description = "\lambda\delta home page"
- title = "\lambda\delta home page"
- logo = "crux"
- head = "The Formal Systems of the λδ (\lambda\delta) Family"
->
- <sitemap name="sitemap"/>
-
- <section9 name="foreword">Foreword</section9>
- <body>
- The formal systems of the λδ (\lambda\delta) family are typed λ-calculi aiming to support
- the foundational frameworks for Mathematics that require an underlying specification language
- (for example the <link to="http://www.math.unipd.it/~maietti/">Minimalist Foundation</link>
- and its predecessors).
- </body>
- <body>
- The λδ family is developed within the
- <link to="http://helm.cs.unibo.it/">Hypertextual Electronic Library of Mathematics</link>
- as a set of machine-checked digital specifications.
- </body>
- <body>
- This is the family logo: <rlink to="images/crux_177.png">crux_177.png</rlink>
- (revised <notice class="alpha" text="2012-09"/>).
- </body>
- <body>
- <notice class="alpha" text="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).
- To change the current font follow:
- "Tools" menu → "Internet Options" entry → "General" tab → "Fonts" button.
- </body>
-
-<!-- ===================================================================== -->
-
- <section9 name="citations">Citations</section9>
- <body>
- This is a list of publications citing λδ documentation.
- </body>
-
- <topitem name="C7">
- C. Dunchev, F. Guidi, C. Sacerdoti Coen, E. Tassi:
- <notice class="alpha">ELPI: Fast, Embeddable, λProlog Interpreter</notice>
- (2015). In proc. of LPAR 20. Lecture Notes in Computer Science, 9450, pp. 460-468. Springer.
- </topitem>
-
- <topitem name="C6">
- A. Asperti, W. Ricciotti, C. Sacerdoti Coen, E. Tassi:
- <notice class="alpha">Formal metatheory of programming languages in the Matita interactive theorem prover</notice>
- (2012). In Journal of Automated Reasoning, 49(3), pp. 427-451. Springer.
- </topitem>
-
- <topitem name="C5">
- M.E. Maietti:
- <notice class="alpha">Consistency of the minimalist foundation with Church thesis and Bar Induction</notice>
- (2012). Submitted article.
- </topitem>
-
- <topitem name="C4">
- W. Ricciotti:
- <notice class="alpha">Theoretical and implementation aspects in the mechanization of the metatheory of programming languages</notice>
- (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">Faithful Reproductions of the Automath Landau Formalization</notice>
- (2011). Technical report.
- </topitem>
-
- <topitem name="C2">
- M.E. Maietti:
- <notice class="alpha">A minimalist two-level foundation for constructive mathematics</notice>
- (2009). In Annals of Pure and Applied Logic, 160(3), pp. 319-354. Elsevier.
- </topitem>
-
- <topitem name="C1">
- V. Rahili:
- <notice class="alpha">First Year Report: Realisability methods of proof and semantics with application to expansion</notice>
- (July 2007). Technical report.
- </topitem>
-
-<!-- ===================================================================== -->
-
- <section9 name="disclaimer">Disclaimer</section9>
- <body>
- The systems of the λδ family <notice class="alpha" text="are not"/> related intentionally to
- any other system having (variations of) the symbols λ and δ in its name or syntax.
- Examples include (but are not limited to):
- </body>
-
- <topitem name="D1">
- <notice class="alpha">λ-δ</notice> of
- A. Church:
- <notice class="alpha">The calculi of lambda-conversion</notice>
- (1941).
- Annals of Mathematics Studies 6.
- Princeton University Press.
- </topitem>
-
- <topitem name="D2">
- <notice class="alpha">∆Λ</notice> of
- N.G. de Bruijn:
- <notice class="alpha">Generalizing Automath by means of a lambda-typed lambda calculus</notice>
- (1987).
- In Lecture Notes in Pure and Applied Mathematics 106, pp. 71-92.
- Marcel Dekker.
- </topitem>
-
- <topitem name="D3">
- <notice class="alpha">λ<sub>∆</sub></notice> of
- N.J. Rehof, M.H. Sørensen:
- <notice class="alpha">The λ<sub>∆</sub>-calculus</notice>
- (1994).
- In Lecture Notes in Computer Science, 789, pp. 516–542.
- Springer.
- </topitem>
-
- <topitem name="D4">
- <notice class="alpha">λ∆</notice> of
- S. Ronchi Della Rocca, L. Paolini:
- <notice class="alpha">The Parametric Lambda Calculus</notice>
- (2004).
- Texts in Theoretical Computer Science, An EATCS Series.
- Springer.
- </topitem>
-
- <topitem name="D5">
- <notice class="alpha">λD</notice> of
- R. Nederpelt, H. Geuvers:
- <notice class="alpha">Type Theory and Formal Proof</notice>
- (2014).
- Cambridge University Press.
- </topitem>
-
- <topitem name="D6">
- <notice class="alpha">Cλξ</notice> of
- N.G. de Bruijn:
- <notice class="alpha">A namefree lambda calculus with facilities for internal definition of expressions and segments</notice>
- (1978).
- TH-report 78-WSK-03.
- Eindhoven University of Technology, Eindhoven.
- </topitem>
-
- <body>
- <img logo="smile"/>
- Moreover, the systems of the λδ family <notice class="alpha" text="are not"/> related intentionally to
- <link to="http://umineko.wikia.com/wiki/Lambdadelta">Lady Lambdadelta</link>,
- the Witch of Certainty of the sound novel
- <link to="https://it.wikipedia.org/wiki/Umineko_no_naku_koro_ni">Umineko no Naku Koro ni</link>.
- </body>
-
- <footer/>
-</page>
table [
class "sky" {
- [ @@("index" "home") * ]
- [ @@("index#foreword" "foreword") * ]
- [ @@("index#citations" "citations") * ]
+ [ @@"home" * ]
+ [ @@("home#foreword" "foreword") * ]
+ [ @@("home#citations" "citations") * ]
}
class "magenta" {
[ @@"news" * ]
}
class "green" {
[ @@"implementation" * ]
- [ @@("implementation#helena" "helena") * ]
+ [ @@("implementation#helena" "helena")
+ @@("osn/" "Open Symbolic Notation (OSN)")
+ * ]
[ @@("implementation#lddl" "library")
"(" ^ @@("static/lddl/" "static LDDL directory") ^ ")"
* ]
</xsl:template>
<xsl:template name="osn-logo">
- <a href="{$baseurl}osn
.html"><img class="w3c"
+ <a href="{$baseurl}osn
/"><img class="w3c"
alt="[Open Symbolic Notation logo]"
title="OSN: Open Symbolic Notation"
src="{$baseurl}images/osn_label.png"
projects / helm.git / commitdiff
