From: Ferruccio Guidi <ferruccio.guidi@unibo.it> Date: Thu, 8 Sep 2011 20:36:58 +0000 (+0000) Subject: initial commit of lambda_delta web site X-Git-Tag: make_still_working~2297 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fba2975ffd09ffb30a60500725c9991421445f37;p=helm.git initial commit of lambda_delta web site (it was not maintained in svn so far) --- diff --git a/helm/www/lambda_delta/documentation.html b/helm/www/lambda_delta/documentation.html new file mode 100644 index 000000000..e7f836acc --- /dev/null +++ b/helm/www/lambda_delta/documentation.html @@ -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> diff --git a/helm/www/lambda_delta/download/automath.sl b/helm/www/lambda_delta/download/automath.sl new file mode 100644 index 000000000..d28950a36 --- /dev/null +++ b/helm/www/lambda_delta/download/automath.sl @@ -0,0 +1,27 @@ +$1 = "Automath"; + +create_syntax_table ($1); + +define_syntax ("{","}",'%', $1); % comments +define_syntax ("#","",'%', $1); % comments +define_syntax ("%","",'%', $1); % comments +define_syntax ("([<", ")]>", '(', $1); % brackets +define_syntax ('"', '"', $1); % strings +define_syntax ("a-zA-Z_0-9`'", 'w', $1); % words +define_syntax (":+-=*@~,;.?", '+', $1); % operators + + +() = define_keywords_n ($1, "EBPN_E", 2, 0); +() = define_keywords_n ($1, "'_E''eb''pn'PRIMPROPTYPE", 4, 0); +() = define_keywords_n ($1, "'prim''prop''type'", 6, 0); + +define Automath_mode () +{ + variable kmap = "Automath"; + + set_mode(kmap, 0x04); + use_syntax_table (kmap); + runhooks("Automath_mode_hook"); +} + +add_mode_for_extension ("Automath", "aut"); diff --git a/helm/www/lambda_delta/download/b3.png b/helm/www/lambda_delta/download/b3.png new file mode 100644 index 000000000..3ed538923 Binary files /dev/null and b/helm/www/lambda_delta/download/b3.png differ diff --git a/helm/www/lambda_delta/download/b4.png b/helm/www/lambda_delta/download/b4.png new file mode 100644 index 000000000..ccfd1a99a Binary files /dev/null and b/helm/www/lambda_delta/download/b4.png differ diff --git a/helm/www/lambda_delta/download/b5.png b/helm/www/lambda_delta/download/b5.png new file mode 100644 index 000000000..30cace1d1 Binary files /dev/null and b/helm/www/lambda_delta/download/b5.png differ diff --git a/helm/www/lambda_delta/download/b9.png b/helm/www/lambda_delta/download/b9.png new file mode 100644 index 000000000..0de559867 Binary files /dev/null and b/helm/www/lambda_delta/download/b9.png differ diff --git a/helm/www/lambda_delta/download/basic_32.png b/helm/www/lambda_delta/download/basic_32.png new file mode 100644 index 000000000..350f6bcb0 Binary files /dev/null and b/helm/www/lambda_delta/download/basic_32.png differ diff --git a/helm/www/lambda_delta/download/bld.pdf b/helm/www/lambda_delta/download/bld.pdf new file mode 100644 index 000000000..469d299ac Binary files /dev/null and b/helm/www/lambda_delta/download/bld.pdf differ diff --git a/helm/www/lambda_delta/download/cie_2010.pdf b/helm/www/lambda_delta/download/cie_2010.pdf new file mode 100644 index 000000000..8afbebb26 Binary files /dev/null and b/helm/www/lambda_delta/download/cie_2010.pdf differ diff --git a/helm/www/lambda_delta/download/crux_16.ico b/helm/www/lambda_delta/download/crux_16.ico new file mode 100644 index 000000000..7323c8af8 Binary files /dev/null and b/helm/www/lambda_delta/download/crux_16.ico differ diff --git a/helm/www/lambda_delta/download/crux_32.png b/helm/www/lambda_delta/download/crux_32.png new file mode 100644 index 000000000..be5524e5e Binary files /dev/null and b/helm/www/lambda_delta/download/crux_32.png differ diff --git a/helm/www/lambda_delta/download/helena.sl b/helm/www/lambda_delta/download/helena.sl new file mode 100644 index 000000000..fc8b1903e --- /dev/null +++ b/helm/www/lambda_delta/download/helena.sl @@ -0,0 +1,28 @@ +$1 = "Helena"; + +create_syntax_table ($1); + +define_syntax ("\\*","*\\",'%', $1); % comments +define_syntax ("([{<", ")]}>", '(', $1); % brackets +define_syntax ('"', '"', $1); % strings +define_syntax ("\\a-zA-Z_0-9", 'w', $1); % words + +set_syntax_flags ($1, 4); + +() = define_keywords_n ($1, "\\ax\\th", 3, 0); +() = define_keywords_n ($1, "\\def", 4, 0); +() = define_keywords_n ($1, "\\cong\\decl\\open", 5, 0); +() = define_keywords_n ($1, "\\close\\graph\\sorts", 6, 0); +() = define_keywords_n ($1, "\\require", 8, 0); +() = define_keywords_n ($1, "\\generate", 9, 0); + +define helena_mode () +{ + variable kmap = "Helena"; + + set_mode(kmap, 0x04); + use_syntax_table (kmap); + runhooks("helena_mode_hook"); +} + +add_mode_for_extension ("helena", "hln"); diff --git a/helm/www/lambda_delta/download/helena_0.8.0.tar.gz b/helm/www/lambda_delta/download/helena_0.8.0.tar.gz new file mode 100644 index 000000000..ef78bc46b Binary files /dev/null and b/helm/www/lambda_delta/download/helena_0.8.0.tar.gz differ diff --git a/helm/www/lambda_delta/download/helena_0.8.1.tar.gz b/helm/www/lambda_delta/download/helena_0.8.1.tar.gz new file mode 100644 index 000000000..c02f7bc14 Binary files /dev/null and b/helm/www/lambda_delta/download/helena_0.8.1.tar.gz differ diff --git a/helm/www/lambda_delta/download/helena_32.png b/helm/www/lambda_delta/download/helena_32.png new file mode 100644 index 000000000..4a065aefe Binary files /dev/null and b/helm/www/lambda_delta/download/helena_32.png differ diff --git a/helm/www/lambda_delta/download/helena_label.png b/helm/www/lambda_delta/download/helena_label.png new file mode 100644 index 000000000..55487ab99 Binary files /dev/null and b/helm/www/lambda_delta/download/helena_label.png differ diff --git a/helm/www/lambda_delta/download/lambda_delta.bib b/helm/www/lambda_delta/download/lambda_delta.bib new file mode 100644 index 000000000..26c994a96 --- /dev/null +++ b/helm/www/lambda_delta/download/lambda_delta.bib @@ -0,0 +1,78 @@ +@incollection{lambdadelta7, + author="F. {Guidi}", + title="{An Efficient Validation Procedure for the Formal System $\lambda\delta$}", + publisher="Centre for Applied Mathematics and Information Technology, Department of Mathematics, University of Azores", + address="Ponta Delgada, Portugal", + editor="F. {Ferreira} and H. {Guerra} and E. {Mayordomo} and J. {Rasga}", + booktitle="Local Proceedings of 6th Conference on Computability in Europe (CiE 2010)", + pages="204-213", + year="2010", + month="July" +} + +@techreport{lambdadelta6, + author="F. {Guidi}", + title="{Landau's ``Grundlagen der Analysis'' from Automath to lambda-delta}", + type="Technical Report", + institution="University of Bologna", + address="Bologna, Italy", + number="UBLCS 2009-16", + year="2009", + month="September" +} + +@article{lambdadelta5, + author="F. {Guidi}", + title="{The Formal System $\lambda\delta$}", + publisher="ACM", + address="New York, NY, USA", + journal="Transactions on Computational Logic", + volume="11", + number="1", + year="2009", + month="October", + pages="Article No. 5" +} + +@incollection{lambdadelta4, + author="F. {Guidi}", + title="{Lambda Types on the Lambda Calculus with Abbreviations}", + publisher="Universit\`a di Siena", + address="Siena, Italy", + editor="S. {Barry Cooper} and T. F. {Kent} and B. {L\"owe} and A. {Sorbi}", @comment="{\"}", + booktitle="Local Proceedings of 3rd Conference on Computability in Europe (CiE 2007) Technical Report 487", + pages="387-387", + year="2007", + month="June" +} + +@techreport{lambdadelta3, + author="F. {Guidi}", + title="{Lambda-Types on the Lambda-Calculus with Abbreviations}", + type="Technical Report", + institution="University of Bologna", + address="Bologna, Italy", + number="UBLCS 2006-25", + year="2006", + month="November" +} + +@techreport{lambdadelta2, + author="F. {Guidi}", + title="{Lambda-Types on the Lambda-Calculus with Abbreviations: a Certified Specification}", + type="Technical Report", + institution="University of Bologna", + address="Bologna, Italy", + number="UBLCS 2006-01", + year="2006", + month="January" +} + +@misc{lambdadelta1, + author="F. {Guidi}", + title="{lambda-delta}", + howpublished="Formal specification with the proof assistant \textsc{coq} 7.3.1", + year="2007", + month="January", + note="Available at the lambda-delta Web site: {http://helm.cs.unibo.it/lambda-delta/}" +} diff --git a/helm/www/lambda_delta/download/lambda_delta.txt b/helm/www/lambda_delta/download/lambda_delta.txt new file mode 100644 index 000000000..26c994a96 --- /dev/null +++ b/helm/www/lambda_delta/download/lambda_delta.txt @@ -0,0 +1,78 @@ +@incollection{lambdadelta7, + author="F. {Guidi}", + title="{An Efficient Validation Procedure for the Formal System $\lambda\delta$}", + publisher="Centre for Applied Mathematics and Information Technology, Department of Mathematics, University of Azores", + address="Ponta Delgada, Portugal", + editor="F. {Ferreira} and H. {Guerra} and E. {Mayordomo} and J. {Rasga}", + booktitle="Local Proceedings of 6th Conference on Computability in Europe (CiE 2010)", + pages="204-213", + year="2010", + month="July" +} + +@techreport{lambdadelta6, + author="F. {Guidi}", + title="{Landau's ``Grundlagen der Analysis'' from Automath to lambda-delta}", + type="Technical Report", + institution="University of Bologna", + address="Bologna, Italy", + number="UBLCS 2009-16", + year="2009", + month="September" +} + +@article{lambdadelta5, + author="F. {Guidi}", + title="{The Formal System $\lambda\delta$}", + publisher="ACM", + address="New York, NY, USA", + journal="Transactions on Computational Logic", + volume="11", + number="1", + year="2009", + month="October", + pages="Article No. 5" +} + +@incollection{lambdadelta4, + author="F. {Guidi}", + title="{Lambda Types on the Lambda Calculus with Abbreviations}", + publisher="Universit\`a di Siena", + address="Siena, Italy", + editor="S. {Barry Cooper} and T. F. {Kent} and B. {L\"owe} and A. {Sorbi}", @comment="{\"}", + booktitle="Local Proceedings of 3rd Conference on Computability in Europe (CiE 2007) Technical Report 487", + pages="387-387", + year="2007", + month="June" +} + +@techreport{lambdadelta3, + author="F. {Guidi}", + title="{Lambda-Types on the Lambda-Calculus with Abbreviations}", + type="Technical Report", + institution="University of Bologna", + address="Bologna, Italy", + number="UBLCS 2006-25", + year="2006", + month="November" +} + +@techreport{lambdadelta2, + author="F. {Guidi}", + title="{Lambda-Types on the Lambda-Calculus with Abbreviations: a Certified Specification}", + type="Technical Report", + institution="University of Bologna", + address="Bologna, Italy", + number="UBLCS 2006-01", + year="2006", + month="January" +} + +@misc{lambdadelta1, + author="F. {Guidi}", + title="{lambda-delta}", + howpublished="Formal specification with the proof assistant \textsc{coq} 7.3.1", + year="2007", + month="January", + note="Available at the lambda-delta Web site: {http://helm.cs.unibo.it/lambda-delta/}" +} diff --git a/helm/www/lambda_delta/download/ld_talk_5s.pdf b/helm/www/lambda_delta/download/ld_talk_5s.pdf new file mode 100644 index 000000000..b7051c919 Binary files /dev/null and b/helm/www/lambda_delta/download/ld_talk_5s.pdf differ diff --git a/helm/www/lambda_delta/download/ld_talk_6s.pdf b/helm/www/lambda_delta/download/ld_talk_6s.pdf new file mode 100644 index 000000000..04fcec20f Binary files /dev/null and b/helm/www/lambda_delta/download/ld_talk_6s.pdf differ diff --git a/helm/www/lambda_delta/download/ld_talk_7s.pdf b/helm/www/lambda_delta/download/ld_talk_7s.pdf new file mode 100644 index 000000000..754547c91 Binary files /dev/null and b/helm/www/lambda_delta/download/ld_talk_7s.pdf differ diff --git a/helm/www/lambda_delta/download/lddl.tar.bz2 b/helm/www/lambda_delta/download/lddl.tar.bz2 new file mode 100644 index 000000000..853e7a907 Binary files /dev/null and b/helm/www/lambda_delta/download/lddl.tar.bz2 differ diff --git a/helm/www/lambda_delta/download/rainbow.png b/helm/www/lambda_delta/download/rainbow.png new file mode 100644 index 000000000..45925baa7 Binary files /dev/null and b/helm/www/lambda_delta/download/rainbow.png differ diff --git a/helm/www/lambda_delta/download/xml_xsl2.png b/helm/www/lambda_delta/download/xml_xsl2.png new file mode 100644 index 000000000..00d82967b Binary files /dev/null and b/helm/www/lambda_delta/download/xml_xsl2.png differ diff --git a/helm/www/lambda_delta/implementation.html b/helm/www/lambda_delta/implementation.html new file mode 100644 index 000000000..c046df27d --- /dev/null +++ b/helm/www/lambda_delta/implementation.html @@ -0,0 +1,274 @@ +<!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><a href="documentation.html">Papers</a></li> + </ul> + <ul> + <li>Resources<br> + </li> + </ul> + </td> + <td style="vertical-align: top; text-align: left;"> + <h3 style="text-align: right;">Computer-checked formal +specifications <img style="width: 37px; height: 37px;" + alt="[Butterfly]" title="Butterfly" src="download/b9.png"></h3> + <span style="font-weight: bold;">Resource +1</span> below provides for the statically generated <span + style="font-weight: bold;">natural language representation</span> of +λδ meta-theory (faster rendering w.r.t. resource 2 below).<br> + <span style="font-weight: bold;">Resource 2</span> below provides +for the dynamically generated <span style="font-weight: bold;">natural +language representation</span> of +λδ meta-theory (powered by the <a href="http://helm.cs.unibo.it/">HELM</a> +rendering engine).<br> +Remarkably λδ was born and developed in the digital format of <span + style="font-weight: bold;">resource 3</span> below, which is not the +formal counterpart of some informal material previously written on +paper (as it happens for most currently digitalized Mathematics).<br> + <ol> + <li><a name="static"></a>F. Guidi: <a + style="font-style: italic;" href="static/matita/LAMBDA-TYPES/">LAMBDA-TYPES</a> +(revised <span style="font-weight: bold;">2008-06</span>). Formal +specification with the proof assistant <a + href="http://matita.cs.unibo.it/">Matita</a> 0.5 (HTML pages generated +by the <a href="http://helm.cs.unibo.it/">HELM</a> +rendering engine)<br> +Here are the most relevant theorems proved in the formal specification: + <ul> + <li><a + href="static/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/pr3/pr3_confluence.con.html">Confluence +of +reduction</a> (Church-Rosser property).</li> + <li><a + href="static/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/props/ty3_correct.con.html">Correctness +of +types</a>.</li> + <li><a + href="static/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/props/ty3_unique.con.html">Uniqueness +of +types +up +to +conversion</a>.<br> + </li> + <li><a + href="static/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3/ty3_sred_pr3.con.html">Subject +reduction +of +the +type +assignment</a>.</li> + <li><a + href="static/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/arity_props/ty3_sn3.con.html">Strong +normalization +of +the +typed +terms</a>.</li> + <li><a + href="static/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/dec/ty3_inference.con.html">Decidability +of +the +type +inference +problem</a>.<br> + <br> + </li> + </ul> + </li> + <li><a name="dynamic"></a>F. Guidi: <a + style="font-style: italic;" + 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/LAMBDA-TYPES/">LAMBDA-TYPES</a> +(revised <span style="font-weight: bold;">2008-06</span>). Formal +specification with the proof assistant <a + href="http://matita.cs.unibo.it/">Matita</a> 0.5 (<a + href="http://helm.cs.unibo.it/">HELM</a> directory).<br> + <br> + </li> + <li><a name="source"></a>F. Guidi: <a + href="http://www.cs.unibo.it/%7Efguidi/download/LAMBDA-TYPES.tgz"><span + style="font-style: italic;">LAMBDA-TYPES</span></a> (revised <span + style="font-weight: bold;">2008-03</span>). +Formal specification with the proof assistant <span + style="font-weight: bold;">Coq 7.3.1</span> (source +proof scripts). <a href="#bibtex">BibTeX entry</a>.<br> + </li> + </ol> + <h3 style="text-align: right;">Tools <img + style="width: 37px; height: 37px;" alt="[Butterfly]" title="Butterfly" + src="download/b5.png"></h3> + <a name="lddl"></a><img style="width: 32px; height: 32px;" + alt="[Crux Logo]" title="The Crux" src="download/crux_32.png"><span + style="font-weight: bold;"> </span>The <span + style="font-weight: bold;"><span style="text-decoration: underline;">λδ +Digital +Library +(LDDL)</span></span> is part of <a href="http://helm.cs.unibo.it/">HELM</a> +and contains a set of +resources expressed in λδ.<br> + <ul> + <li><span style="font-weight: bold;">Contents:</span> Landau's "<span + style="font-style: italic;">Grundlagen der Analysis</span>" (from +Jutting's specification in <a href="http://www.win.tue.nl/automath/">Automath</a>).<br> + <span style="font-weight: bold;"></span></li> + </ul> + <ul> + <li><span style="font-weight: bold;">Access:</span> <a + href="static/lddl/">static pages</a> (updated <span + style="font-weight: bold;">2010-11</span>), <a + href="download/lddl.tar.bz2">data set</a> (updated <span + style="font-weight: bold;">2010-11</span>), <a + href="http://helm.cs.unibo.it/lambda-delta/xml">HELM server URL</a> +(updated <span style="font-weight: bold;">2010-11</span>).</li> + </ul> + <ul> + <li><span style="font-weight: bold;">Examples:</span> <a + href="static/lddl/brg-si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">Grundlagen's +definition +"t234"</a> (in "basic_rg" λδ), <a + href="static/lddl/crg-si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">Grundlagen's +definition +"t234"</a> (in "complete_rg" λδ).<br> + </li> + </ul> + <br> + <a name="helena"></a><span style="font-weight: bold;"><img + style="width: 32px; height: 32px;" alt="[Helena Logo]" title="Helena" + src="download/helena_32.png"> <span + style="text-decoration: underline;">Helena</span></span> is a λδ +processor, +implemented in <a href="http://caml.inria.fr/">Caml</a> as a part of +the <a href="http://helm.cs.unibo.it/">HELM</a> software, meant for +testing the stable features of the calculus as well as the unstable +ones.<br> +The processor source code is available in the directory <a + href="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&path=%2Ftrunk%2Fhelm%2Fsoftware%2Flambda-delta%2F&rev=0&sc=0">/trunk/helm/software/lambda-delta/</a> +of the <a href="http://helm.cs.unibo.it/software/index.html">HELM Svn +repository</a>. The Svn revisions containing the stable versions +of Helena are indicated below. <br> + <ul> + <li><span style="font-weight: bold;">Version 0.8.1 (2010-11).</span> +Exploits a subset of "complete_rg" λδ as the intermediate language. +Features importation from ".hln" files containing λδ textual syntax. +The overall validation speed of the "<span style="font-style: italic;">Grundlagen +der +Analysis</span>" increases of 22% with respect to version 0.8.0. [Svn +revision: 11032] (<a href="download/helena_0.8.1.tar.gz">archived +source code</a>) + <ul> + <li><span style="font-weight: bold;">2009-12.</span> Helena +appears in F. Wiedijk's <a + href="http://www.cs.ru.nl/%7Efreek/digimath/index.html">index of +computer math systems</a>.</li> + </ul> + </li> + </ul> + <ul> + <li><a style="font-weight: bold;" + href="documentation.html#ublcs-2009-16">Version 0.8.0</a><span + style="font-weight: bold;"> (2009-09).</span> 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>. [Svn +revision: 10304] (<a href="download/helena_0.8.0.tar.gz">archived +source code</a>)<br> + <ul> + <li><span style="font-weight: bold;">2009-09.</span> +Jutting's specification of Landau's "<span style="font-style: italic;">Grundlagen +der +Analysis</span>" enters λδ Digital Library.<br> + <span style="font-weight: bold;"></span></li> + <li><span style="font-weight: bold;">2009-06.</span> +Jutting's specification of Landau's "<span style="font-style: italic;">Grundlagen +der +Analysis</span>" is +successfully processed, enabling sort inclusion<span + style="font-weight: bold;"></span>.</li> + </ul> + </li> + </ul> + <h3 style="text-align: right;">Other resources <img + style="width: 37px; height: 37px;" alt="[Butterfly]" title="Butterfly" + src="download/b4.png"></h3> + <ul> + <li><a name="bibtex"></a>A +BibTeX database of λδ documentation: <a + href="download/lambda_delta.bib"><span style="font-style: italic;">lambda-delta.bib</span></a>, + + <a style="font-style: italic;" + href="download/lambda_delta.txt">lambda-delta.txt</a> (revised <span + style="font-weight: bold;">2010-07</span>).</li> + </ul> + <ul> + <li>A <a href="http://www.jedsoft.org/jed/">Jed mode</a> for +editing ".hln" files (containing λδ textual syntax): <a + style="font-style: italic;" href="download/helena.sl">helena.sl</a> +(revised <span style="font-weight: bold;">2010-11</span>).</li> + </ul> + <ul> + <li>A <a href="http://www.jedsoft.org/jed/">Jed mode</a> for +editing ".aut" files (containing <a + href="http://www.win.tue.nl/automath/">Automath</a> textual syntax): <a + style="font-style: italic;" href="download/automath.sl">automath.sl</a> +(revised <span style="font-weight: bold;">2008-07</span>).</li> + </ul> + <ul> + <li>A logo for "basic" λδ: <a href="download/bld.pdf"><span + style="font-style: italic;">bld.pdf</span></a> (revised <span + style="font-weight: bold;">2008-07</span>).<br> + </li> + </ul> + </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> diff --git a/helm/www/lambda_delta/index.html b/helm/www/lambda_delta/index.html new file mode 100644 index 000000000..abc24b14e --- /dev/null +++ b/helm/www/lambda_delta/index.html @@ -0,0 +1,111 @@ +<!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>Foreword</li> + </ul> + <ul> + <li><a href="news.html">News</a></li> + </ul> + <ul> + <li><a href="documentation.html">Papers</a></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;">Foreword <img + style="width: 37px; height: 37px;" alt="[Butterfly]" title="Butterfly" + src="download/b9.png"></h3> +The formal system λδ +(lambda-delta) is a typed lambda calculus that pursues the static and +dynamic unification of terms, types, environments and contexts while +enjoying a well-conceived meta-theory, which includes the commonly +desired properties.<br> + <br> +λδ takes some features from the calculi of the Automath family and +some from the pure type systems, but it differs from both in that it +does not include the Î construction while it provides for an +abbreviation mechanism at the level of terms.<br> + <br> +λδ features explicit type annotations, which are borrowed from +realistic type checker implementations and with which type checking is +reduced to type inference.<br> + <br> +The reduction steps of λδ include β-contraction, δ-expansion, +ζ-contraction and θ-swap. On the other hand, +η-contraction is not included.<br> + <br> +The meta-theory of λδ includes important properties such as the +confluence of reduction, the correctness of types, the +uniqueness of types up to conversion, the subject reduction of the type +assignment, the strong normalization of the typed terms. The +decidability of type inference and of type checking come as corollaries.<br> + <br> +λδ features uniformly dependent types and a predicative abstraction +mechanism, so the calculus can serve as a formal specification language +for the type theories that need a predicative foundation. λδ is +expected to have the expressive power of λâ.<br> + <h3 style="text-align: right;">Notice +for +the +Internet +Explorer +user <img style="width: 37px; height: 37px;" alt="[Butterfly]" + title="Butterfly" src="download/b3.png"></h3> +To view this site +correctly, please select a font with <a href="http://www.unicode.org/">Unicode</a> +support.<br> +For example <span style="font-weight: bold;">Lucida Sans Unicode</span> +(it should be already installed on your system).<br> +To change the current font follow: <br> + <span style="font-weight: bold;">"Tools" menu â "Internet +Options" entry â "General" tab â "Fonts" button.</span><br> + </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> diff --git a/helm/www/lambda_delta/news.html b/helm/www/lambda_delta/news.html new file mode 100644 index 000000000..fc6d4d244 --- /dev/null +++ b/helm/www/lambda_delta/news.html @@ -0,0 +1,234 @@ +<!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>News</li> + </ul> + <ul> + <li><a href="documentation.html">Papers</a></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;">News <img + style="width: 37px; height: 37px;" alt="[Butterfly]" title="Butterfly" + src="download/b5.png"></h3> + <ul> + <li><span style="font-weight: bold;">December 2010.</span> +Permanent λδ URL acquired: <a href="http://lambda-delta.info">http://lambda-delta.info</a> +(pointing at this site). <br> + <span style="font-weight: bold;"></span></li> + </ul> + <ul> + <li><span style="font-weight: bold;">November 2010.</span> <span + style="font-style: italic;">Helena 0.8.1</span> is released. <br> + </li> + </ul> + <ul> + <li><span style="font-weight: bold;">September 2009.</span> <span + style="font-style: italic;">Helena 0.8.0</span> is released and the <a + href="implementation.html#lddl">λδ Digital Library</a> is +started.<br> + <span style="font-weight: bold;"></span></li> + </ul> + <ul> + <li><span style="font-weight: bold;">June 2009.</span> <span + style="font-style: italic;">Helena</span>, A <a + href="implementation.html#helena">validator for </a><a + href="implementation.html#helena">λδ</a><span + style="font-style: italic;"></span>, <span style="font-style: italic;"></span>is +available +as a +part of the <a href="http://helm.cs.unibo.it/">HELM</a> software. <br> + </li> + </ul> + <span style="font-weight: bold;"></span> + <ul> + <li><span style="font-weight: bold;">September 2008.</span> +This site is online.<br> + </li> + </ul> + <span style="font-weight: bold;"></span> + <ul> + <li><span style="font-weight: bold;">July 2008.</span> <a + href="documentation.html#tocl1">First journal paper on λδ</a> accepted +for publication.</li> + </ul> + <ul> + <li><span style="font-weight: bold;">July 2008.</span> First <a + href="http://helm.cs.unibo.it/procedural/">procedural +reconstruction</a> in <a href="http://matita.cs.unibo.it/">Matita 0.5</a> +of the <a href="implementation.html#source">λδ proof scripts in +Coq 7.3.1</a>.<br> + </li> + </ul> + <ul> + <li><span style="font-weight: bold;">June 2008.</span> The <a + href="implementation.html#static">HTML +pages of the specification of λδ in Matita 0.5</a> are online.<br> + <span style="font-weight: bold;"></span></li> + </ul> + <ul> + <li><span style="font-weight: bold;">March 2008.</span> An +improvement of the +specification of λδ in Coq 7.3.1 begins: + <ul> + <li>native type assignment with new rules for application: <span + style="font-style: italic;">nty</span> (it replaces <span + style="font-style: italic;">ty3</span>);<br> + </li> + <li>parallel conversion on focalized terms: <span + style="font-style: italic;">fpcs</span> (it replaces <span + style="font-style: italic;"></span><span style="font-style: italic;">pc3</span>); + + + + + + + + <br> + </li> + <li>new weak parallel reduction on environments: <span + style="font-style: italic;">wcpr</span> <span + style="font-style: italic;"></span>(it is based on <span + style="font-style: italic;">fpr</span> and replaces <span + style="font-style: italic;">wcpr0</span>); <br> + </li> + <li>parallel reduction on focalized terms: <span + style="font-style: italic;">fpr</span> and <span + style="font-style: italic;">fprs</span> (they replace <span + style="font-style: italic;"></span><span style="font-style: italic;"></span><span + style="font-style: italic;">pr2</span>, <span + style="font-style: italic;">pr3</span>); <br> + </li> + </ul> + <ul> + <li>new thinning relation: <span + style="font-style: italic;">drop</span> +(it replaces the old <span style="font-style: italic;">drop</span>, <span + style="font-style: italic;">clear</span>, <span + style="font-style: italic;">getl</span>, <span + style="font-style: italic;">cimp</span>, <span + style="font-style: italic;">drop1</span>);</li> + <li>new shift function: <span style="font-style: italic;">shift</span>: +(it +replaces + <span style="font-style: italic;">app1</span>);</li> + <li>new length function for environments: <span + style="font-style: italic;">clen</span>;<br> + </li> + <li>new relocation function: <span + style="font-style: italic;">lift</span> (it replaces old <span + style="font-style: italic;">lift</span>, <span + style="font-style: italic;">lift1</span>);<br> + </li> + <li>new term structure with polarity indicators and no +distinction between binding and flat items;</li> + <li>new general theory of relocation (comprises new +relocation functions: <span style="font-style: italic;">s</span>, <span + style="font-style: italic;">r</span>);</li> + <li>we removed context-free reduction and conversion (<span + style="font-style: italic;">pr0</span>, <span + style="font-style: italic;">pr1</span>, <span + style="font-style: italic;">pc1</span>);<br> + </li> + <li>we removed greedy substitution (<span + style="font-style: italic;"></span><span style="font-style: italic;">csubst0</span>, + + + <span style="font-style: italic;">csubst1</span>, <span + style="font-style: italic;">fsubst0</span>, <span + style="font-style: italic;">subst0</span>, <span + style="font-style: italic;">subst1</span>);<br> + </li> + <li>we removed level indicators on environments (<span + style="font-style: italic;">cbk</span>).</li> + </ul> + </li> + </ul> + <ul> + <li><span style="font-weight: bold;">September 2007.</span> +The <a href="implementation.html#dynamic">specification of λδ in +Matita 0.4</a> is online.<br> + </li> + </ul> + <ul> + <li><span style="font-weight: bold;">December 2005.</span> <a + href="documentation.html#bologna1">First communication on λδ</a>.<br> + </li> + </ul> + <ul> + <li><span style="font-weight: bold;">May 2004.</span> The <a + href="implementation.html#source">specification of λδ in +Coq 7.3.1</a> begins.<br> + </li> + </ul> + <h3 style="text-align: right;">Visibility <img + style="width: 37px; height: 37px;" alt="[Butterfly]" title="Butterfly" + src="download/b4.png"></h3> + <ul> + <li><span style="font-weight: bold;">November 2010.</span> The <a + href="http://www.google.com/">Google</a> +search <span style="color: rgb(255, 0, 0);">formal system lambda delta</span> +gives 8 resources about λδ as the first results.<br> + </li> + </ul> + <ul> + <li><span style="font-weight: bold;">November 2010.</span> The <a + href="http://www.yahoo.com/">Yahoo</a> +search <span style="color: rgb(255, 0, 0);">formal system lambda delta</span> +gives 4 resources and 2 sub-resources about λδ as the first results.</li> + </ul> + </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>