X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Flambda_delta%2Fimplementation.html;fp=helm%2Fwww%2Flambda_delta%2Fimplementation.html;h=c046df27de484088ea1564cf8136a7f2400ec928;hb=fba2975ffd09ffb30a60500725c9991421445f37;hp=0000000000000000000000000000000000000000;hpb=b4240d93f7fd4c3e60d3495dc558edfc0e0f48e7;p=helm.git diff --git a/helm/www/lambda_delta/implementation.html b/helm/www/lambda_delta/implementation.html new file mode 100644 index 000000000..c046df27d --- /dev/null +++ b/helm/www/lambda_delta/implementation.html @@ -0,0 +1,274 @@ + + +
+ +
+
|
+
+ Computer-checked formal +specifications+ Resource +1 below provides for the statically generated natural language representation of +λδ meta-theory (faster rendering w.r.t. resource 2 below).+ Resource 2 below provides +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). +
Tools+ The λδ +Digital +Library +(LDDL) is part of HELM +and contains a set of +resources expressed in λδ.+
+ Helena is a λδ +processor, +implemented in Caml as a part of +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/ +of the HELM Svn +repository. The Svn revisions containing the stable versions +of Helena are indicated below. +
Other resources+
|
+