]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/www/lambda_delta/documentation.html
initial commit of lambda_delta web site
[helm.git] / helm / www / lambda_delta / documentation.html
diff --git a/helm/www/lambda_delta/documentation.html b/helm/www/lambda_delta/documentation.html
new file mode 100644 (file)
index 0000000..e7f836a
--- /dev/null
@@ -0,0 +1,353 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
+<html>
+<head>
+  <meta content="text/html; charset=UTF-8" http-equiv="content-type">
+  <title>lambda-delta home page</title>
+  <meta content="Ferruccio Guidi" name="author">
+  <meta content="The formal system lambda-delta" name="description">
+  <link rel="shortcut icon" href="download/crux_16.ico">
+</head>
+<body>
+<div style="text-align: center;">
+<br>
+<a href="http://lambda-delta.info"><img alt="[Crux Logo]"
+ title="The Crux" src="download/crux_32.png"
+ style="border: 0px solid ; width: 32px; height: 32px;"></a>
+<h1>The Formal System λδ (lambda-delta)<br>
+</h1>
+<h2>Towards the unification of terms, types, environments and contexts</h2>
+<img style="width: 95%; height: 4px;" alt="[Separator]"
+ title="Separator" src="download/rainbow.png"><br>
+<table
+ style="text-align: left; width: 95%; margin-left: auto; margin-right: auto;"
+ border="0" cellpadding="2" cellspacing="20">
+  <tbody>
+    <tr>
+      <td style="vertical-align: top;">
+      <ul>
+        <li><a href="index.html">Foreword</a></li>
+      </ul>
+      <ul>
+        <li><a href="news.html">News</a></li>
+      </ul>
+      <ul>
+        <li>Papers</li>
+      </ul>
+      <ul>
+        <li><a href="implementation.html">Resources</a><br>
+        </li>
+      </ul>
+      </td>
+      <td style="vertical-align: top; text-align: left;">
+      <h3 style="text-align: right;">Documentation <img
+ style="width: 37px; height: 37px;" alt="[Butterfly]" title="Butterfly"
+ src="download/b5.png"></h3>
+Currently the <span style="font-weight: bold;">main source of
+information</span> on λδ (version 1) is <span
+ style="font-weight: bold;">Resource
+1.1</span> below.<br>
+A <span style="font-weight: bold;">summary</span> of basic λδ (version
+1) is found in <span style="font-weight: bold;">Resource 1.5</span>
+below.<br>
+      <h3><img style="width: 32px; height: 32px;"
+ alt="[Basic lambda-delta Logo]" title="Basic lambda-delta"
+ src="download/basic_32.png"> Basic λδ version 2:</h3>
+      <table style="text-align: left; width: 100%;" border="0"
+ cellpadding="2" cellspacing="2">
+        <tbody>
+          <tr>
+            <td style="vertical-align: top;">2.1.<br>
+            </td>
+            <td style="vertical-align: top;">F. Guidi: <a
+ href="download/cie_2010.pdf"><span style="font-style: italic;">An
+Efficient
+Validation Procedure for the Formal System </span><span
+ style="font-style: italic;">λδ</span></a><span
+ style="font-style: italic;"></span>
+(<span style="font-weight: bold;">2010-07</span>). In <span
+ style="font-style: italic;">CiE 2010 Local Proceedings</span>.
+University of Azores, CMATI Booklet, pp. 204-213. <a
+ href="implementation.html#bibtex">BibTeX entry</a>.<br>
+            <br>
+            </td>
+          </tr>
+          <tr>
+            <td style="vertical-align: top;">2.2.<br>
+            </td>
+            <td style="vertical-align: top;"> <a name="ublcs-2009-16"></a>F.
+Guidi:
+
+
+
+
+
+
+
+
+            <a
+ href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2009.bib?ncstrl.cabernet//BOLOGNA-UBLCS-2009-16"><span
+ style="font-style: italic;">Landau's
+"Grundlagen der Analysis" from Automath to lambda-delta</span></a> (<span
+ style="font-weight: bold;">2009-09)</span>. University of
+Bologna, technical report UBLCS-2009-16. <a
+ href="implementation.html#bibtex">BibTeX entry</a>.<br>
+            <br>
+            </td>
+          </tr>
+          <tr>
+            <td style="vertical-align: top;">2.3.<br>
+            </td>
+            <td style="vertical-align: top;">F. Guidi: <a
+ href="download/ld_talk_7s.pdf"><span style="font-style: italic;">An
+Efficient
+Validation Procedure for the Formal System λδ</span></a> (<span
+ style="font-weight: bold;">2010-07</span>). Presentation
+at
+CiE
+2010
+(slides).<br>
+            <br>
+            </td>
+          </tr>
+          <tr>
+            <td style="vertical-align: top;">2.4.<br>
+            </td>
+            <td style="vertical-align: top;">F. Guidi: <a
+ href="download/ld_talk_6s.pdf"><span style="font-style: italic;">A
+Validator
+for the Formal System λδ</span></a> (revised <span
+ style="font-weight: bold;">2010-02</span>). Presentation
+at
+the
+University
+of
+Bologna
+(slides). </td>
+          </tr>
+        </tbody>
+      </table>
+      <h3><img style="width: 32px; height: 32px;"
+ alt="[Basic lambda-delta Logo]" title="Basic lambda-delta"
+ src="download/basic_32.png"> Basic λδ version 1:</h3>
+      <table style="text-align: left; width: 100%;" border="0"
+ cellpadding="2" cellspacing="2">
+        <tbody>
+          <tr>
+            <td style="vertical-align: top;">1.1.<br>
+            </td>
+            <td style="vertical-align: top;"><a name="tocl1"></a>F.
+Guidi: <a href="http://doi.acm.org/10.1145/1614431.1614436"><span
+ style="font-style: italic;">The Formal System λδ</span></a> (<span
+ style="font-weight: bold;">2009-10</span>). In ACM ToCL 11(1), Article
+No. 5 (<a href="http://tocl.acm.org/accepted/335guidi.pdf">accepted</a>
+            <span style="font-weight: bold;">2008-07</span>). CoRR
+identifier <a href="http://arxiv.org/abs/cs/0611040"><span
+ style="font-style: italic;"></span>cs/0611040</a> [v10] (revised <span
+ style="font-weight: bold;">2008-09</span>). <a
+ href="implementation.html#bibtex">BibTeX
+entry</a>.<br>
+            <br>
+            </td>
+          </tr>
+          <tr>
+            <td style="vertical-align: top;">1.2.<br>
+            </td>
+            <td style="vertical-align: top;">F. Guidi: <a
+ href="http://www.cs.unibo.it/%7Efguidi/download/cie_2007.pdf"><span
+ style="font-style: italic;">Lambda Types on the Lambda Calculus with
+Abbreviations</span></a> (<span style="font-weight: bold;">2007-06</span>).
+In
+
+
+
+
+
+
+
+
+
+
+
+
+            <span style="font-style: italic;">CiE 2007 Local Proceedings</span>.
+University
+of
+Siena,
+technical
+report
+487,
+p.
+387
+(abstract
+of
+a
+presentation).
+
+
+
+
+
+
+            <a href="implementation.html#bibtex">BibTeX
+entry</a>.<br>
+            <br>
+            </td>
+          </tr>
+          <tr>
+            <td style="vertical-align: top;">1.3.<br>
+            </td>
+            <td style="vertical-align: top;">F. Guidi: <a
+ href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2006.bib?ncstrl.cabernet//BOLOGNA-UBLCS-2006-25"><span
+ style="font-style: italic;">Lambda Types on the Lambda Calculus with
+Abbreviations</span></a> (<span style="font-weight: bold;">2006-11</span>).
+University
+of
+Bologna,
+technical
+report
+UBLCS-2006-25.
+
+
+
+
+
+
+
+
+
+
+
+
+
+            <a href="implementation.html#bibtex">BibTeX
+entry</a>.<br>
+            <br>
+            </td>
+          </tr>
+          <tr>
+            <td style="vertical-align: top;">1.4.<br>
+            </td>
+            <td style="vertical-align: top;">F. Guidi: <a
+ style="font-style: italic;"
+ href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2006.bib?ncstrl.cabernet//BOLOGNA-UBLCS-2006-01">Lambda
+Types
+on
+the
+Lambda
+Calculus
+with
+Abbreviations:
+a
+Certified
+Specification</a> (<span style="font-weight: bold;">2006-01</span>).
+University of
+Bologna, technical report UBLCS-2006-01. <a
+ href="implementation.html#bibtex">BibTeX entry</a>.<br>
+            <br>
+            </td>
+          </tr>
+          <tr>
+            <td style="vertical-align: top;">1.5.<br>
+            </td>
+            <td style="vertical-align: top;">F. Guidi: <a
+ style="font-style: italic;" href="download/ld_talk_5s.pdf">The
+Formal
+System lambda-delta</a>
+(<span style="font-weight: bold;">2008-10</span>). Presentation at
+"Advances in Constructive Topology and Logical Foundations" (slides).<br>
+            <br>
+            </td>
+          </tr>
+          <tr>
+            <td style="vertical-align: top;">1.6.<br>
+            </td>
+            <td style="vertical-align: top;">F. Guidi: <a
+ href="http://www.cs.unibo.it/%7Efguidi/download/ld-talk-4.pdf"><span
+ style="font-style: italic;">Towards the Unification of Terms, Types
+and Contexts</span></a> (<span style="font-weight: bold;">2008-03</span>).
+Presentation
+at
+Types
+2008
+(slides).<br>
+            <br>
+            </td>
+          </tr>
+          <tr>
+            <td style="vertical-align: top;">1.7.<br>
+            </td>
+            <td style="vertical-align: top;">F. Guidi: <a
+ href="http://www.cs.unibo.it/%7Efguidi/download/ld-talk-3.pdf"><span
+ style="font-style: italic;">Lambda Types on the Lambda Calculus with
+Abbreviations</span></a> (<span style="font-weight: bold;">2007-06</span>).
+Presentation
+at
+CiE
+2007
+(slides).<br>
+            <br>
+            </td>
+          </tr>
+          <tr>
+            <td style="vertical-align: top;">1.8.<br>
+            </td>
+            <td style="vertical-align: top;">F. Guidi: <a
+ href="http://www.cs.unibo.it/%7Efguidi/download/ld-talk-2.pdf"><span
+ style="font-style: italic;">Lambda Tipi sul Lambda Calcolo con
+Abbreviazioni</span></a> (<span style="font-weight: bold;">2007-01</span>).
+Presentation
+at
+the
+University
+of
+Padova
+(slides
+
+
+
+
+
+
+            <span style="font-weight: bold;">in
+Italian</span>).<br>
+            <br>
+            </td>
+          </tr>
+          <tr>
+            <td style="vertical-align: top;">1.9.<br>
+            </td>
+            <td style="vertical-align: top;"><a name="bologna1"></a>F.
+Guidi: <a
+ href="http://www.cs.unibo.it/%7Efguidi/download/ld-talk-1.pdf"><span
+ style="font-style: italic;">Lambda Tipi sul Lambda Calcolo con
+Abbreviazioni: una Specifica Certificata</span></a> (<span
+ style="font-weight: bold;">2005-12</span>). Presentation at
+the University of Bologna (slides <span style="font-weight: bold;">in
+Italian</span>).<br>
+            </td>
+          </tr>
+        </tbody>
+      </table>
+      </td>
+    </tr>
+  </tbody>
+</table>
+<br>
+<a href="http://validator.w3.org/check?uri=referer"><img
+ alt="[Valid HTML 4.01 Transitional]"
+ title="Valid HTML 4.01 Transitional"
+ src="http://www.w3.org/Icons/valid-html401"
+ style="border: 0px solid ; width: 88px; height: 31px;"></a> <a
+ href="http://www.anybrowser.org/campaign/"><img
+ alt="[Use Any Browser Here]" title="Use Any Browser Here"
+ src="http://www.cs.unibo.it/%7Efguidi/download/globe-trans.png"
+ style="border: 0px solid ; width: 147px; height: 42px;"></a> <img
+ style="width: 88px; height: 31px;" alt="[PNG Used Here]"
+ title="PNG Used Here]"
+ src="http://www.cs.unibo.it/%7Efguidi/download/PNGnow2.png"><br>
+<br>
+Last update 2010-12-14 by <a href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
+Guidi</a><br>
+</div>
+</body>
+</html>