-
|
-
- 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-
| + home + | ++ news + | ++ documentation + | ++ specification + | +
+ + |
+ + implementation + | +
+ foreword + | ++ milestones + | ++ version 2 + | ++ version 2 + | +(background - core - applications) | ++ library + | +||
+ citations + | ++ visibility + | ++ version 1 + | ++ version 1 + | +
+ + |
+ + helena |
-
-
- Last update 2012-12-02 by Ferruccio - Guidi