@@ -40,21 +36,16 @@
|
Computer-checked formal
- specifications
+ specifications
Resource
- 1 below provides for the statically generated natural language
+ 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
+ for the dynamically generated natural
language representation of
- λδ meta-theory (powered by the HELM
+ λδ meta-theory (powered by the HELM
rendering engine).
Remarkably, λδ was born and developed in the digital
format of resource 3
@@ -64,51 +55,42 @@
paper (as it happens for most currently digitalized
Mathematics).
- - F. Guidi: lambdadelta
+
- F. Guidi: lambdadelta
(revised 2011-09).
Formal
- specification for Matita 0.5
+ specification for Matita 0.5
(HTML pages generated
by the HELM
- rendering engine)
+ rendering engine)
Here are the most relevant theorems proved in the
formal specification:
- - F. Guidi: lambdadelta
+
- F. Guidi: lambdadelta
(revised 2011-09).
Formal
- specification for Matita 0.5 (HELM directory).
-
+ specification for Matita 0.5 (HELM directory).
+ Currently, the HELM rendering engine is offline.
+
- - F. Guidi: lambdadelta_1
- (revised 2011-09).
+
- F. Guidi: lambdadelta_1
+ (revised 2012-10).
Formal
specification for Coq
7.3.1
@@ -139,52 +116,35 @@ Formal
proof scripts). BibTeX entry.
- Tools
- The λδ
+ Tools
+ The λδ
Digital
Library
- (LDDL) is part of HELM
+ (LDDL) is part of HELM
and contains a set of
resources expressed in λδ.
- Contents:
Landau's "Grundlagen
der Analysis" (from
- Jutting's specification in Automath).
+ Jutting's specification in Automath).
- Helena
+ Helena
is a λδ
processor,
implemented in Caml
@@ -194,10 +154,8 @@ href="static/lddl/crg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.ht
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
+ 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
@@ -215,19 +173,16 @@ href="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&path=%2Ftrunk%
intermediate language.
Features importation from ".hln" files containing λδ
textual syntax.
- The overall validation speed of the "Grundlagen
+ The overall validation speed of the "Grundlagen
der
Analysis" increases of 22% with respect to
version 0.8.0. [Svn
- revision: 11032] (archived
+ revision: 11032] (archived
source code)
- - Version 0.8.0 (2009-09).
+
- Version 0.8.0 (2009-09).
Supports
"basic_rg" λδ with naive implementation of
impredicative sort
inclusion. Features
- importation from Automath
+ importation from Automath
and exportation to XML.
[Svn
- revision: 10304] (archived
+ revision: 10304] (archived
source code)
- 2009-09.
- Jutting's specification of Landau's "Grundlagen
+ Jutting's specification of Landau's "Grundlagen
der
Analysis" enters λδ Digital Library.
- 2009-06.
- Jutting's specification of Landau's "Grundlagen
+ Jutting's specification of Landau's "Grundlagen
der
Analysis" is
- successfully processed, enabling sort inclusion.
+ successfully processed, enabling sort inclusion.
- Other resources
+ Other resources
- A Jed mode
for
- editing ".hln" files (containing λδ textual syntax): helena.sl
+ editing ".hln" files (containing λδ textual syntax): helena.sl
(revised 2010-11).
@@ -306,20 +244,12 @@ computer
|