X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Flambdadelta%2Fdocumentation.html;h=56ff9c6fb5ce7dedfa397287b5a162c668174192;hb=f6923ff81abc829b20c6d01801fd6b98ab88cd65;hp=d855689c24c8b81c98f44d2df3c43ebb7ad42ba9;hpb=691c330235597faab8ad7be34242bc545d4c4023;p=helm.git diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index d855689c2..56ff9c6fb 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -1,355 +1,303 @@ - - -
- -
+
|
+
+ Documentation
+
+The main source of
+information is Resource P8. |
-
| R5. |
-
- Documentation
- Currently the main
- source of
- information on λδ (version 1) is Resource
- 1.1 below.- A summary of - basic λδ (version - 1) is found in Resource - 1.5 - below. -
- |
+
2.1. - |
- F.
- Guidi: An
- Efficient
- Validation Procedure for the Formal System λδ
- (2010-07).
- In CiE 2010
- Local Proceedings.
- University of Azores, CMATI Booklet, pp. 204-213.
- BibTeX entry. - - |
- |
2.2. - |
- F. -Guidi: + | F.
+Guidi: An Efficient Validation Procedure for the
+Formal System λδ (2010-07).
+In
+ CiE 2010 Local Proceedings.
+University
+of
+Azores, CMATI Booklet, pp. 204-213. BibTeX entry. + + |
+
R4. + |
+ F.
+Guidi: Landau's "Grundlagen der Analysis" from
+Automath to lambda-delta (2009-09).
+
+University
+of
+Bologna, technical report UBLCS-2009-16. BibTeX entry. + + |
+ |
P8. + |
+ F.Guidi:
+ The Formal System λδ and the "Three
+Problems" (2014-06).
+Presentation at University of Bologna (slides). + + |
+ |
P7. + |
+ F.
+Guidi: An Efficient Validation Procedure for the
+Formal System λδ (2010-07).
+
+Presentation
+at
+CiE 2010 (slides). + + |
+ |
P6. + |
+ F. +Guidi: A Validator for the Formal System λδ +(revised 2010-02). +Presentation at University of Bologna (slides). | +
J1. + |
+ F.
+Guidi: The Formal System λδ (2009-11). In ACM ToCL 11(1), pp.
+5:1-5:37 (accepted
+ 2008-07). CoRR
+identifier cs/0611040 [v10] (revised 2008-09). BibTeX entry. + + |
+
R3. + |
+ F.
+Guidi: Lambda Types on the Lambda Calculus with
+Abbreviations (2007-06).
+
+In
+ CiE 2007 Local Proceedings.
+University
+of
+Siena, technical report 487, p. 387 (abstract of a
+presentation). BibTeX entry. + + |
+
R2. + |
+ F.
+Guidi: Lambda Types on the Lambda Calculus with
+Abbreviations (2006-11).
+University
+of
+Bologna, technical report UBLCS-2006-25. BibTeX entry. + + |
+
R1. + |
+ F.
+Guidi: Lambda
+Types
+on
+the Lambda Calculus with Abbreviations: a Certified
+Specification (2006-01).
+University of Bologna, technical report UBLCS-2006-01. BibTeX entry. + + |
+
P5. + |
+ F.
+Guidi: The
+Formal
+System
+ λδ (2008-10). Presentation at "Advances
+in Constructive Topology and Logical Foundations" (slides). + + |
+
P4. + |
+ F.
+Guidi: Towards the Unification of Terms, Types
+and Contexts (2008-03).
+Presentation
+at
+Types 2008 (slides). + + |
+
P3. + |
+ F.
+Guidi: Lambda Types on the Lambda Calculus with
+Abbreviations (2007-06).
+Presentation
+at
+CiE 2007 (slides). + + |
+
P2. + |
+ F.
+Guidi: Lambda Tipi sul Lambda Calcolo con
+Abbreviazioni (2007-01).
- Landau's
- "Grundlagen der Analysis" from Automath to
- lambdadelta (2009-09).
- University of
- Bologna, technical report UBLCS-2009-16. BibTeX entry. - - |
-
2.3. - |
- F.
- Guidi: An
- Efficient
- Validation Procedure for the Formal System λδ
- (2010-07).
- Presentation
- at
- CiE
- 2010
- (slides). - - |
-
2.4. - |
- F. - Guidi: A - Validator - for the Formal System λδ (revised 2010-02). - Presentation - at - the - University - of - Bologna - (slides). | -
1.1. - |
- F.
-Guidi:
- The Formal System
- λδ (2009-10). In ACM ToCL 11(1),
- Article
- No. 5 (accepted
- 2008-07).
- CoRR
- identifier cs/0611040
- [v10] (revised 2008-09).
- BibTeX
- entry. - - |
-
1.2. - |
- F.
- Guidi: Lambda
- Types on the Lambda Calculus with
- Abbreviations (2007-06).
- In CiE 2007
- Local Proceedings.
- University
- of
- Siena,
- technical
- report
- 487,
- p.
- 387
- (abstract
- of
- a
- presentation). BibTeX
- entry. - - |
-
1.3. - |
- F.
- Guidi: Lambda Types on
- the Lambda Calculus with
- Abbreviations (2006-11).
- University
- of
- Bologna,
- technical
- report
- UBLCS-2006-25. BibTeX
- entry. - - |
-
1.4. - |
- F.
- Guidi: Lambda
- Types
- on
- the
- Lambda
- Calculus
- with
- Abbreviations:
- a
- Certified
- Specification (2006-01).
- University of
- Bologna, technical report UBLCS-2006-01. BibTeX entry. - - |
-
1.5. - |
- F.
- Guidi: The
- Formal
- System lambdadelta
- (2008-10).
- Presentation at
- "Advances in Constructive Topology and Logical
- Foundations" (slides). - - |
-
1.6. - |
- F.
- Guidi: Towards
- the Unification of Terms, Types
- and Contexts (2008-03).
- Presentation
- at
- Types
- 2008
- (slides). - - |
-
1.7. - |
- F.
- Guidi: Lambda
- Types on the Lambda Calculus with
- Abbreviations (2007-06).
- Presentation
- at
- CiE
- 2007
- (slides). - - |
-
1.8. - |
- F.
- Guidi: Lambda
- Tipi sul Lambda Calcolo con
- Abbreviazioni (2007-01).
- Presentation
- at
- the
- University
- of
- Padova
- (slides in
- Italian). - - |
-
1.9. - |
- F.
-Guidi:
- Lambda Tipi sul
- Lambda Calcolo con
- Abbreviazioni: una Specifica Certificata
- (2005-12).
- Presentation at
- the University of Bologna (slides in
- Italian). - |
-