X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fdocumentation.html;h=5f7506bd5b8bb7beaf00f0f2a23d2447cceaadd5;hb=e36a0eced135e6f1b79d06c78a408918f65376b6;hp=38d99b003b434f22c4818005996ef44292537fba;hpb=7562d9781dc4f351ddc3b2f8edd21f4976621948;p=helm.git diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index 38d99b003..5f7506bd5 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -23,7 +23,7 @@
[Spacer]
-
+

@@ -45,9 +45,15 @@
- + +
+ + implementation + +
+ @@ -63,9 +69,13 @@ version 2 (background - core - applications) - + +
+ + library + (static LDDL directory) @@ -80,20 +90,21 @@ version 1 - -
- - + (background - core) + (static HELM directory) + helena + +
+
- -
Documentation [spacer] +
Documentation [spacer]
-
+
BibTeX database of λδ documentation: download lambdadelta.bib, @@ -101,13 +112,35 @@ lambdadelta.txt (revised 2014-10).
- -
+
+ [spacer] λδ version 3 (proposed)
+
+ The main source of information is J4. +
+
+ + + + + + + + + + +
+ J4. + F. Guidi: A Verified Translation of Landau's "Grundlagen" from Automath into a Pure Type System, via λδ (2015-02). Submitted to JFR, Univerity of Bologna.
+ +
+
+
+
[spacer] λδ version 2 (active)
-
+
The main source of information is J2.
-
+
@@ -197,14 +230,13 @@
- -
+
[spacer] λδ version 1 (superseded)
-
+
The main source of information is J1. A summary is available in P5.
-
+
@@ -331,8 +363,7 @@
- -
+
[Spacer]
@@ -358,6 +389,6 @@

-
Last update: Tue, 04 Nov 2014 16:28:51 +0100
- +
Last update: Sat, 21 Feb 2015 23:38:38 +0100
+