-
| + home + | ++ news + | ++ specification + | +
+ + |
+
+ + |
+ + documentation + | ++ implementation + | +
+ + |
+
+ foreword + | ++ milestones + | ++ version 2 + | +(background - core - applications) | +
+ + |
+ + version 2 + | ++ helena + | ++ Open Symbolic Notation (OSN) + | +|
+ citations + | ++ visibility | -
- 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-
| + version 1 | +(background - core) | +(static HELM directory) | ++ version 1 + | ++ library + | +(static LDDL directory) |
-
-
- Last update 2012-12-01 by Ferruccio - Guidi