-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
+<!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">
+ <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;">2.1.<br>
+ <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;">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.
+ <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 (in
+ progress):</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;"><a name="ldp7"></a>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="ldp6"></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>
+ <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;"><a name="ldt7"></a>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;"><a name="ldt6"></a>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
+ (dismissed):</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="ldp5"></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;"><a name="ldp4"></a>F.
+ Guidi: <a href="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;"><a name="ldp3"></a>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;"><a name="ldp2"></a>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;"><a name="ldt5"></a>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;"><a name="ldt4"></a>F.
+ Guidi: <a href="download/ld_talk_4s.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;"><a name="ldt3"></a>F.
+ Guidi: <a href="download/ld_talk_3s.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;"><a name="ldt2"></a>F.
+ Guidi: <a href="download/ld_talk_2s.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="ldt1"></a>F.
+Guidi:
+ <a href="download/ld_talk_1s.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>
- </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>
+ <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="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 2012-02-24 by <a
+ href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
+ Guidi</a><br>
+ </div>
+ </body>
</html>
projects / helm.git / blobdiff