X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambda_delta%2Fimplementation.html;h=6fc317e77f9fde4a701e26cfc51b11011328d070;hb=96c5bba006710411b469c2ddf5439cf337a8e6b9;hp=c046df27de484088ea1564cf8136a7f2400ec928;hpb=fba2975ffd09ffb30a60500725c9991421445f37;p=helm.git diff --git a/helm/www/lambda_delta/implementation.html b/helm/www/lambda_delta/implementation.html index c046df27d..6fc317e77 100644 --- a/helm/www/lambda_delta/implementation.html +++ b/helm/www/lambda_delta/implementation.html @@ -2,9 +2,9 @@ - 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:
- 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&param.thmedia-type=text/html&param.thkeys=T1%2CT2%2CL%2CE&param.embedkeys=d_c%2CTC1%2CHC2%2CL&param.thencoding=UTF-8&prop.encoding=UTF-8&prop.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&param.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&param.encoding=UTF-8&param.media-type=text/html&param.keys=d_c%2CC1%2CHC2%2CL&profile=default&param.profile=default&param.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), HELM server URL -(updated 2010-11).
- 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" Î»Î´).

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

The Formal System Î»Î´ (lambda_delta)

Towards the unification of terms, types, environments and contexts

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