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=0000000000000000000000000000000000000000;hb=207a37632296335aa8db7b22482f91634f74e4e1;hp=598daae78cd41d6df3a1258116d5db75e3e797df;hpb=691c330235597faab8ad7be34242bc545d4c4023;p=helm.git diff --git a/helm/www/lambda_delta/implementation.html b/helm/www/lambda_delta/implementation.html deleted file mode 100644 index 598daae78..000000000 --- a/helm/www/lambda_delta/implementation.html +++ /dev/null @@ -1,325 +0,0 @@ - - -
- -
-
|
-
- 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/helena/ - of the HELM - Svn - repository. The Svn revisions containing the stable - versions - of Helena are indicated below. -
Other resources-
|
-