-
|
-
- 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: - - - - - - - - - + | + home + | ++ news + | ++ documentation + | ++ specification + | +
+ + |
+ + implementation + | +
+ foreword + | ++ milestones + | ++ version 2 + | ++ version 2 + | +(background - core - applications) | ++ library + | +||
+ notice + | ++ visibility + | ++ version 1 + | ++ version 1 + | +
+ + |
+ + helena + | +
Documentation
+
+ ![lambdadelta butterfly [spacer]](http://lambdadelta.info/images/b4.png)
+ BibTeX database of λδ documentation:
+ lambdadelta.bib,
+ lambdadelta.txt
+ (revised 2014-10).
+
+
+
+
λδ version 2 (in progress)
+ ![lambdadelta butterfly [spacer]](http://lambdadelta.info/images/b4.png)
+ The main source of information is P8.
+
+
+
+
+
+
- Landau's
- "Grundlagen der Analysis" from Automath to
- lambda-delta (2009-09).
- University of
- Bologna, technical report UBLCS-2009-16. BibTeX entry.+ R5. + | +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). | +
+ |
+ + |
+
+ V2. + | +F. Guidi: lambdadelta_2 (revised 2014-10). Formal specification for the proof assistant Matita 0.99.2 (scripts). BibTeX entry. | +
+ |
+ + |
+
-
-
-
-
-
-
Basic λδ version 1
- (dismissed):
- 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). - |
-
+
λδ version 1 (dismissed)
+ ![lambdadelta butterfly [spacer]](http://lambdadelta.info/images/b6.png)
+ The main source of information is J1.
+ A summary is available in P5.
+
+
+
+
+
-
-
![PNG Used Here] [PNG Used Here]](http://www.cs.unibo.it/%7Efguidi/images/PNGnow2.png)
-
- Last update 2012-12-01 by Ferruccio - Guidi
-
-
\ No newline at end of file
+
+ + J1. + | +F. Guidi: The Formal System λδ (2009-11). In 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). Presentation at University of Padova (slides in Italian). | +
+ |
+ + |
+
+ P1. + | +F. Guidi: Lambda Tipi sul Lambda Calcolo con Abbreviazioni: una Specifica Certificata (2005-12). Presentation at University of Bologna (slides in Italian). | +
+ |
+ + |
+
+ V1. + | +F. Guidi: lambdadelta_1 (revised 2012-10). Formal specification for the proof assistant Coq 7.3.1 (scripts). BibTeX entry. | +
+ |
+ |
-
![Use Any Browser Here [Use Any
- Browser Here]](images/globe_trans.png)
![PNG Used Here] [PNG Used Here]](http://www.cs.unibo.it/%7Efguidi/images/PNGnow2.png)
-
- Last update 2012-12-01 by Ferruccio - Guidi
+
+
+ ![lambdadelta rainbow rule [Spacer]](http://lambdadelta.info/images/rainbow.png)
+
+
+
+ +
+
+
+ +
Last update: Thu, 09 Oct 2014 20:11:23 +0200
+
+