-
![[Crux Logo]](images/crux_32.png "The Crux")
+
The Formal System λδ (\lambda\delta)
Towards the unification of terms, types, environments and
@@ -55,42 +55,42 @@
paper (as it happens for most currently digitalized
Mathematics).
- - F. Guidi: lambdadelta
+
- F. Guidi: lambdadelta
(revised 2011-09).
Formal
specification for Matita 0.5
(HTML pages generated
by the HELM
- rendering engine)
+ rendering engine)
Here are the most relevant theorems proved in the
formal specification:
- - Confluence
+
- Confluence
of
reduction (Church-Rosser property).
- - Correctness
+
- Correctness
of
types.
- - Uniqueness
+
- Uniqueness
of
types
up
to
conversion.
- - Subject
+
- Subject
reduction
of
the
type
assignment.
- - Strong
+
- Strong
normalization
of
the
typed
terms.
- - Decidability
+
- Decidability
of
the
type
@@ -104,9 +104,10 @@
(revised 2011-09).
Formal
specification for Matita 0.5 (HELM directory).
-
+ Currently, the HELM rendering engine is offline.
+
- - F. Guidi: lambdadelta_1
+
- F. Guidi: lambdadelta_1
(revised 2012-10).
Formal
specification for Coq
@@ -130,13 +131,14 @@ Formal
- - Access: static pages (updated 2012-10), data set (updated 2012-10), HELM server URL
+
- Access: static pages (updated 2012-10), data set (updated 2012-10), HELM server URL
(updated 2012-10).
- - Examples: Grundlagen's
+
- Examples: Grundlagen's
definition
- "t234" (in "basic_rg" λδ), Grundlagen's
+ "t234" (in "basic_rg" λδ), Grundlagen's
definition
"t234" (in "complete_rg" λδ).
@@ -175,7 +177,7 @@ Formal
der
Analysis" increases of 22% with respect to
version 0.8.0. [Svn
- revision: 11032] (archived
+ revision: 11032] (archived
source code)
- 2009-12.
@@ -196,7 +198,7 @@ computer
importation from Automath
and exportation to XML.
[Svn
- revision: 10304] (archived
+ revision: 10304] (archived
source code)
- 2009-09.
@@ -215,21 +217,21 @@ computer
Other resources ![[Butterfly]](images/b4.png "Butterfly")
- A
- BibTeX database of λδ documentation: lambdadelta.bib,
- lambdadelta.txt
+ BibTeX database of λδ documentation: lambdadelta.bib,
+ lambdadelta.txt
(revised 2012-10).
- A Jed mode
for
- editing ".hln" files (containing λδ textual syntax): helena.sl
+ editing ".hln" files (containing λδ textual syntax): helena.sl
(revised 2010-11).
- A Jed mode
for
editing ".aut" files (containing Automath
- textual syntax): automath.sl
+ textual syntax): automath.sl
(revised 2008-07).
@@ -246,8 +248,8 @@ computer
Transitional" src="http://www.w3.org/Icons/valid-html401" style="border: 0px solid ; width: 88px; height: 31px;"> ![[Use Any
Browser Here]](images/globe_trans.png "Use Any Browser Here")
![[PNG Used Here]](images/PNGnow2.png "PNG Used Here")
- Last update 2012-12-02 by Ferruccio
+ Last update 2014-02-22 by Ferruccio
Guidi
+ rendering engine) Here are the most relevant theorems proved in the formal specification:
-
-
- Confluence
+
- Confluence of reduction (Church-Rosser property).
-- Correctness +
- Correctness of types.
-- Uniqueness +
- Uniqueness of types up to conversion.
-
- Subject +
- Subject reduction of the type assignment.
-- Strong +
- Strong normalization of the typed terms.
-- Decidability +
- Decidability of the type @@ -104,9 +104,10 @@ (revised 2011-09). Formal specification for Matita 0.5 (HELM directory).
-
-
+ Currently, the HELM rendering engine is offline.
+
- F. Guidi: lambdadelta_1 +
- F. Guidi: lambdadelta_1 (revised 2012-10). Formal specification for Coq @@ -130,13 +131,14 @@ Formal
-
-
- Access: static pages (updated 2012-10), data set (updated 2012-10), HELM server URL +
- Access: static pages (updated 2012-10), data set (updated 2012-10), HELM server URL (updated 2012-10).
-
-
- Examples: Grundlagen's
+
- Examples: Grundlagen's definition - "t234" (in "basic_rg" λδ), Grundlagen's + "t234" (in "basic_rg" λδ), Grundlagen's definition "t234" (in "complete_rg" λδ).
@@ -175,7 +177,7 @@ Formal der Analysis" increases of 22% with respect to version 0.8.0. [Svn - revision: 11032] (archived + revision: 11032] (archived source code)
- 2009-12.
@@ -196,7 +198,7 @@ computer
importation from Automath
and exportation to XML.
[Svn
- revision: 10304] (archived
+ revision: 10304] (archived
source code)
- 2009-09.
@@ -215,21 +217,21 @@ computer
Other resources
- A - BibTeX database of λδ documentation: lambdadelta.bib, - lambdadelta.txt + BibTeX database of λδ documentation: lambdadelta.bib, + lambdadelta.txt (revised 2012-10).
- A Jed mode for - editing ".hln" files (containing λδ textual syntax): helena.sl + editing ".hln" files (containing λδ textual syntax): helena.sl (revised 2010-11).
- A Jed mode for editing ".aut" files (containing Automath - textual syntax): automath.sl + textual syntax): automath.sl (revised 2008-07).
-
@@ -246,8 +248,8 @@ computer
Transitional" src="http://www.w3.org/Icons/valid-html401" style="border: 0px solid ; width: 88px; height: 31px;">
- Last update 2012-12-02 by Ferruccio + Last update 2014-02-22 by Ferruccio Guidi
- 2009-09.
@@ -215,21 +217,21 @@ computer
- Examples: Grundlagen's definition - "t234" (in "basic_rg" λδ), Grundlagen's + "t234" (in "basic_rg" λδ), Grundlagen's definition "t234" (in "complete_rg" λδ).