- lambda-delta home page
+ lambda_delta home page
-
+
@@ -13,7 +13,7 @@
-
The Formal System λδ (lambda-delta)
+
The Formal System λδ (lambda_delta)
Towards the unification of terms, types, environments and contexts
natural
language representation of
λδ meta-theory (powered by the HELM
rendering engine).
-Remarkably λδ was born and developed in the digital format of resource 3 below, which is not the
formal counterpart of some informal material previously written on
paper (as it happens for most currently digitalized Mathematics).
F. Guidi: LAMBDA-TYPES
-(revised 2008-06). Formal
+ style="font-style: italic;" href="static/matita/lambda_delta/">lambda_delta
+(revised 2011-09). Formal
specification with the proof assistant Matita 0.5 (HTML pages generated
by the HELM
@@ -66,15 +66,15 @@ rendering engine)
Here are the most relevant theorems proved in the formal specification:
F. Guidi: LAMBDA-TYPES
-(revised 2008-06). Formal
+ href="http://mowgli.cs.unibo.it:58080/apply?keys=RT&xmluri=http://helm.cs.unibo.it/helm//html/folder/index.html&prop.media-type=text/html¶m.thmedia-type=text/html¶m.thkeys=T1%2CT2%2CL%2CE¶m.embedkeys=d_c%2CTC1%2CHC2%2CL¶m.thencoding=UTF-8&prop.encoding=UTF-8&prop.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN¶m.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN¶m.encoding=UTF-8¶m.media-type=text/html¶m.keys=d_c%2CC1%2CHC2%2CL&profile=default¶m.profile=default¶m.CICURI=theory:/matita/lambda_delta/">lambda_delta
+(revised 2011-09). Formal
specification with the proof assistant Matita 0.5 (HELM directory).
F. Guidi: LAMBDA-TYPES (revised 2008-03).
+ href="download/lambda_delta_1.tar.gz">lambda_delta_1 (revised 2011-09).
Formal specification with the proof assistant Coq 7.3.1 (source
proof scripts). BibTeX entry.
@@ -148,7 +148,7 @@ Jutting's specification in Automath2010-11), data set (updated 2010-11), HELM server URL
+ href="http://lambda-delta.info/xml">HELM server URL
(updated 2010-11).
@@ -172,7 +172,7 @@ the HELM software, meant for
testing the stable features of the calculus as well as the unstable
ones.
The processor source code is available in the directory /trunk/helm/software/lambda-delta/
+ href="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&path=%2Ftrunk%2Fhelm%2Fsoftware%2Flambda_delta%2F&rev=0&sc=0">/trunk/helm/software/lambda_delta/
of the HELM Svn
repository. The Svn revisions containing the stable versions
of Helena are indicated below.
@@ -224,10 +224,11 @@ successfully processed, enabling sort inclusion
A
BibTeX database of λδ documentation: lambda-delta.bib,
+ href="download/lambda_delta.bib">lambda_delta.bib,
+
lambda-delta.txt (revised lambda_delta.txt (revised 2010-07).