X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fdocumentation.html;h=4e85dbaae92d472ab7deb644c18440ba68754c85;hb=22d35425b8f5f7e479db3be59b73f76d77ae6711;hp=d855689c24c8b81c98f44d2df3c43ebb7ad42ba9;hpb=691c330235597faab8ad7be34242bc545d4c4023;p=helm.git diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index d855689c2..4e85dbaae 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -1,26 +1,22 @@ - - - - lambdadelta home page + + + + + λδ home page + - - - - + +

- [Crux Logo] -

The Formal System λδ (lambdadelta)
+ [Crux Logo] +

The Formal System λδ (\lambda\delta)

Towards the unification of terms, types, environments and contexts

- [Separator]
- + [Separator]
+
@@ -39,36 +35,28 @@ -

Documentation [Butterfly]

+

Documentation [Butterfly]

Currently the main source of - information on λδ (version 1) is Resource - 1.1 below.
+ information on λδ (version 1) is Resource + 1.9 below.
A summary of basic λδ (version 1) is found in Resource 1.5 below.

[Basic
-                  lambdadelta Logo] Basic λδ version 2 (in + lambdadelta Logo]" title="Basic lambdadelta" src="images/basic_32.png"> Basic λδ version 2 (in progress):

- +
- - - -
2.1.
+
2.4.
F. - Guidi: An + Guidi: An Efficient - Validation Procedure for the Formal System λδ + Validation Procedure for the Formal System λδ (2010-07). In CiE 2010 Local Proceedings. @@ -78,7 +66,7 @@
2.2.
+
2.3.
F. Guidi: @@ -93,24 +81,19 @@ Guidi: - Landau's + Landau's "Grundlagen der Analysis" from Automath to - lambdadelta (2009-09). + lambda-delta (2009-09). University of - Bologna, technical report UBLCS-2009-16. BibTeX entry.
+ Bologna, technical report UBLCS-2009-16. BibTeX entry.

2.3.
+
2.2.
F. - Guidi: An + Guidi: An Efficient Validation Procedure for the Formal System λδ (2010-07). @@ -123,14 +106,12 @@ href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2009.bib?ncstrl.cabernet//BO
2.4.
+
2.1.
F. - Guidi: A + Guidi: A Validator - for the Formal System λδ (revised 2010-02). + for the Formal System λδ (revised 2010-02). Presentation at the @@ -142,30 +123,22 @@ href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2009.bib?ncstrl.cabernet//BO

[Basic
-                  lambdadelta Logo] Basic λδ version 1 + lambdadelta Logo]" title="Basic lambdadelta" src="images/basic_32.png"> Basic λδ version 1 (dismissed):

- +
- - - - @@ -248,10 +211,9 @@ href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2006.bib?ncstrl.cabernet//BO - - - - @@ -336,20 +290,13 @@ Guidi:
1.1.
+
1.9.
F. Guidi: - The Formal System - λδ (2009-10). In ACM ToCL 11(1), - Article - No. 5 (accepted + The Formal System + λδ (2009-11). In ACM ToCL 11(1), + pp. 5:1-5:37 + (accepted 2008-07). CoRR - identifier cs/0611040 + identifier cs/0611040 [v10] (revised 2008-09). BibTeX entry.
@@ -173,14 +146,12 @@ Guidi:
1.2.
+
1.8.
F. - Guidi: Lambda + Guidi: Lambda Types on the Lambda Calculus with - Abbreviations (2007-06). + Abbreviations (2007-06). In CiE 2007 Local Proceedings. University @@ -194,39 +165,33 @@ Guidi: (abstract of a - presentation). BibTeX + presentation). BibTeX entry.

1.3.
+
1.7.
F. - Guidi: Lambda Types on + Guidi: Lambda Types on the Lambda Calculus with - Abbreviations (2006-11). + Abbreviations (2006-11). University of Bologna, technical report - UBLCS-2006-25. BibTeX + UBLCS-2006-25. BibTeX entry.

1.4.
+
1.6.
F. - Guidi: Lambda + Guidi: Lambda Types on the @@ -236,11 +201,9 @@ href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2006.bib?ncstrl.cabernet//BO Abbreviations: a Certified - Specification (2006-01). + Specification (2006-01). University of - Bologna, technical report UBLCS-2006-01. BibTeX entry.
+ Bologna, technical report UBLCS-2006-01. BibTeX entry.

1.5.
F. - Guidi: The + Guidi: The Formal - System lambdadelta + System λδ (2008-10). Presentation at "Advances in Constructive Topology and Logical @@ -260,14 +222,12 @@ href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2006.bib?ncstrl.cabernet//BO
1.6.
+
1.4.
F. - Guidi: Towards + Guidi: Towards the Unification of Terms, Types - and Contexts (2008-03). + and Contexts (2008-03). Presentation at Types @@ -277,14 +237,12 @@ href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2006.bib?ncstrl.cabernet//BO
1.7.
+
1.3.
F. - Guidi: Lambda + Guidi: Lambda Types on the Lambda Calculus with - Abbreviations (2007-06). + Abbreviations (2007-06). Presentation at CiE @@ -294,14 +252,12 @@ href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2006.bib?ncstrl.cabernet//BO
1.8.
+
1.2.
F. - Guidi: Lambda + Guidi: Lambda Tipi sul Lambda Calcolo con - Abbreviazioni (2007-01). + Abbreviazioni (2007-01). Presentation at the @@ -314,18 +270,16 @@ href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2006.bib?ncstrl.cabernet//BO
1.9.
+
1.1.
F. Guidi: - Lambda Tipi sul + Lambda Tipi sul Lambda Calcolo con Abbreviazioni: una Specifica Certificata (2005-12). Presentation at - the University of Bologna (slides in + the University of Bologna (slides in Italian).

- [Valid HTML 4.01 Transitional] [Use Any
-          Browser Here] [PNG Used Here]
+ [Valid HTML 4.01 Transitional] [Use Any
+          Browser Here] [PNG Used Here]

- Last update 2012-12-01 by Ferruccio + Last update 2012-12-02 by Ferruccio Guidi
- - + + +