-
| + home + | ++ news + | ++ documentation + | ++ specification + | +
+ + |
+
+ + |
+ + implementation + | +
+ + |
+
+ foreword + | ++ milestones + | ++ version 2 + | ++ version 2 + | +(background - core - applications) | +
+ + |
+ + library + | +(static LDDL directory) | +|
+ citations + | ++ visibility + | ++ version 1 | -
- 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 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
-
| + version 1 + | +(background - core) | +(static HELM directory) | ++ helena + | +
+ |
-
![Use Any Browser Here [Use Any
- Browser Here]](download/globe_trans.png)
![PNG Used Here [PNG Used Here]](download/PNGnow2.png)
-
- Last update 2012-12-01 by Ferruccio - Guidi