-
|
-
- Documentation- Currently the main - source of - information on λδ (version 1) is Resource - 1.9 below.- A summary of - basic λδ (version - 1) is found in Resource - 1.5 - below. - Basic λδ version 2 (in - progress):-
Documentation
+
+
+ BibTeX database of λδ documentation:
+ lambdadelta.bib,
+ lambdadelta.txt
+ (revised 2014-07).
+
+
+
+ λδ version 2 (in progress)
+
+ 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.
- - |
- |||||||||||||||||||||||||||||||||||||||||||
2.2. - |
- F.
- Guidi: An
- Efficient
- Validation Procedure for the Formal System λδ
- (2010-07).
- Presentation
- at
- CiE
- 2010
- (slides). - - |
- |||||||||||||||||||||||||||||||||||||||||||
2.1. - |
- F. - Guidi: A - Validator - for the Formal System λδ (revised 2010-02). - Presentation - at - the - University - of - Bologna - (slides). | -
Basic λδ version 1 - (dismissed):
-1.9. - |
- 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. - - |
-
1.8. - |
- 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.7. - |
- F.
- Guidi: Lambda Types on
- the Lambda Calculus with
- Abbreviations (2006-11).
- University
- of
- Bologna,
- technical
- report
- UBLCS-2006-25. BibTeX
- entry. - - |
-
1.6. - |
- 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 λδ
- (2008-10).
- Presentation at
- "Advances in Constructive Topology and Logical
- Foundations" (slides). - - |
-
1.4. - |
- F.
- Guidi: Towards
- the Unification of Terms, Types
- and Contexts (2008-03).
- Presentation
- at
- Types
- 2008
- (slides). - - |
-
1.3. - |
- F.
- Guidi: Lambda
- Types on the Lambda Calculus with
- Abbreviations (2007-06).
- Presentation
- at
- CiE
- 2007
- (slides). - - |
-
1.2. - |
- F.
- Guidi: Lambda
- Tipi sul Lambda Calcolo con
- Abbreviazioni (2007-01).
- Presentation
- at
- the
- University
- of
- Padova
- (slides in
- Italian). - - |
-
1.1. - |
- 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)
+
+ The main source of information is J1.
+ A summary is available in P5.
+
+
+
+
+
-
-
-
- Last update 2012-12-02 by Ferruccio - Guidi
-
-
+ + 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. | +
+ |
+ |
-
-
- Last update 2012-12-02 by Ferruccio - Guidi
+
+
+
+
+
+
+ +
+
+
+ +
Last update: Sat, 04 Oct 2014 22:58:58 +0200
+
+