X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambda_delta%2Fimplementation.html;h=12458806e6ed391ace7df458b53bad75a2e5f372;hb=fca65d71d40cce00c0ac601e8c1626ba085c26e2;hp=27fbff71b43c1b251070d84449ea533c8fd5e62d;hpb=0a5a2f3cf0e3f748feb5beaad413181163504509;p=helm.git
diff --git a/helm/www/lambda_delta/implementation.html b/helm/www/lambda_delta/implementation.html
index 27fbff71b..12458806e 100644
--- a/helm/www/lambda_delta/implementation.html
+++ b/helm/www/lambda_delta/implementation.html
@@ -51,14 +51,14 @@ for the dynamically generated 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:
- Confluence
+ href="static/matita/lambda_delta/Basic_1/pr3/pr3/pr3_confluence.con.html">Confluence
of
reduction (Church-Rosser property).
- Correctness
+ href="static/matita/lambda_delta/Basic_1/ty3/props/ty3_correct.con.html">Correctness
of
types.
- Uniqueness
+ href="static/matita/lambda_delta/Basic_1/ty3/props/ty3_unique.con.html">Uniqueness
of
types
up
@@ -82,21 +82,21 @@ to
conversion.
- Subject
+ href="static/matita/lambda_delta/Basic_1/ty3/pr3/ty3_sred_pr3.con.html">Subject
reduction
of
the
type
assignment.
- Strong
+ href="static/matita/lambda_delta/Basic_1/ty3/arity_props/ty3_sn3.con.html">Strong
normalization
of
the
typed
terms.
- Decidability
+ href="static/matita/lambda_delta/Basic_1/ty3/dec/ty3_inference.con.html">Decidability
of
the
type
@@ -108,17 +108,17 @@ problem.
- 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.
@@ -145,18 +145,18 @@ Jutting's specification in Automath
- Access: static pages (updated 2010-11), 2011-09), data set (updated 2010-11), 2011-09), HELM server URL
-(updated 2010-11).
+(updated 2011-09).
- Examples: Grundlagen's
+ href="static/lddl/brg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">Grundlagen's
definition
"t234" (in "basic_rg" λδ), Grundlagen's
+ href="static/lddl/crg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">Grundlagen's
definition
"t234" (in "complete_rg" λδ).
@@ -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%2Fhelena%2F&rev=0&sc=0">/trunk/helm/software/helena/
of the HELM Svn
repository. The Svn revisions containing the stable versions
of Helena are indicated below.
@@ -188,7 +188,7 @@ source code)
@@ -226,9 +226,10 @@ successfully processed, enabling sort inclusionlambda_delta.bib,
+
lambda_delta.txt (revised 2010-07).
+ style="font-weight: bold;">2011-09).