The Formal System Î»Î´ (\lambda\delta)
-

Towards the unification of terms, types, environments and contexts

- - - - - - - -

Foreword

News

Papers

Resources
-

Documentation

Basic Î»Î´ version -2 (in progress):

-The main source of -information is Resource P8.
-
- + + + + + + + + + + \lambda\delta home page + + + + + + +

+ +

The Formal System Î»Î´ (\lambda\delta)

+
+

- - + + + - + + + + - + + + + + + + + +

R5. +	+ home	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. - +	+ news +	+ documentation +	+ implementation +	+
R4. +	+ Foreword +	+ Milestones +	+ Version 2 +	+ Version 2 +	+ Background + Core + Applications	F. -Guidi: Landau's "Grundlagen der Analysis" from -Automath to lambda-delta (2009-09). +
+ Notice +	+ Visibility +	+ Version 1 +	+ Version 1 +	+ +

+ -University -of -Bologna, technical report UBLCS-2009-16. BibTeX entry.
-

Documentation [spacer]

+ BibTeX database of Î»Î´ documentation: + lambdadelta.bib, + lambdadelta.txt + (revised 2012-10). +

+ +

Î»Î´ version 2 (in progress)

+ The main source of information is P8. +

+ + + + + - - + + + - - + + + + + + + + + + + + + + + + + + + + - + + + + -

+ 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.
P8. +	+	+	F.Guidi: - The Formal System Î»Î´ and the "Three -Problems" (2014-06). -Presentation at University of Bologna (slides). - +
+ 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.
P7. +	+	+	F. -Guidi: An Efficient Validation Procedure for the -Formal System Î»Î´ (2010-07). - -Presentation -at -CiE 2010 (slides). - +
+ 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).
+	+
P6. +	+ V2. +	F. Guidi: lambdadelta_2 (revised 2014-07). Formal specification for the proof assistant Matita 0.99.2 (scripts). BibTeX entry.
+	+	F. -Guidi: A Validator for the Formal System Î»Î´ -(revised 2010-02). -Presentation at University of Bologna (slides).

Basic Î»Î´ version -1 (dismissed):

-The main source of -information is Resource J1. -A summary is found in Resource P5.
-
- + + +

Î»Î´ version 1 (dismissed)

+ The main source of information is J1. + A summary is available in P5. +

- - + + + - - + + + - - + + + - - + + + - - + + + - - + + + - - + + + - - + + + - - + + +

J1. +	+ 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. - +	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. +	+ 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. - +	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. +	+ R2.	F. -Guidi: Lambda Types on the Lambda Calculus with -Abbreviations (2006-11). - -University -of -Bologna, technical report UBLCS-2006-25. BibTeX entry. - +	F. Guidi: Lambda Types on the Lambda Calculus with Abbreviations (2006-11). University of Bologna, technical report UBLCS-2006-25. BibTeX entry.
+	+
R1. +	+ 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. - +	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. +	+ P5.	F. -Guidi: The - -Formal -System - Î»Î´ (2008-10). Presentation at "Advances -in Constructive Topology and Logical Foundations" (slides). - +	F. Guidi: The Formal System Î»Î´ (2008-10). Presentation at Advances in Constructive Topology and Logical Foundations (slides).
+	+
P4. +	+ P4.	F. -Guidi: Towards the Unification of Terms, Types -and Contexts (2008-03). - -Presentation -at -Types 2008 (slides). - +	F. Guidi: Towards the Unification of Terms, Types and Contexts (2008-03). Presentation at Types 2008 (slides).
+	+
P3. +	+ P3.	F. -Guidi: Lambda Types on the Lambda Calculus with -Abbreviations (2007-06). - -Presentation -at -CiE 2007 (slides). - +	F. Guidi: Lambda Types on the Lambda Calculus with Abbreviations (2007-06). Presentation at CiE 2007 (slides).
+	+
P2. +	+ P2.	F. -Guidi: Lambda Tipi sul Lambda Calcolo con -Abbreviazioni (2007-01). - -Presentation -at -University of Padova (slides in -Italian). - +	F. Guidi: Lambda Tipi sul Lambda Calcolo con Abbreviazioni (2007-01). Presentation at University of Padova (slides in Italian).
+	+
P1. +	+ P1.	F. -Guidi: Lambda Tipi sul Lambda Calcolo con -Abbreviazioni: una Specifica Certificata (2005-12). Presentation at University -of Bologna (slides in -Italian). +	F. Guidi: Lambda Tipi sul Lambda Calcolo con Abbreviazioni: una Specifica Certificata (2005-12). Presentation at University of Bologna (slides in Italian).
+	+