]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/www/lambdadelta/web/home/documentation_3.tbl
documentation update
[helm.git] / helm / www / lambdadelta / web / home / documentation_3.tbl
index ec291e009dfa9b49ac0d3a1bcb72a42ee6813e19..b4dd848a600b4c991f8a07497920310483a22095 100644 (file)
@@ -1,12 +1,13 @@
 name "documentation_3"
 
 table {
-   [ { name "ldJ4" "<span class=\"emph alpha\">J4.</span>" "" } {
+   [ { name "ldJ3a" "<span class=\"emph alpha\">J3a.</span>" "" } {
      "F. Guidi:" +
-     @@("download/gda.pdf"
-     "A Verified Translation of Landau's \"Grundlagen\" from Automath into a Pure Type System, via λδ") +
-     "(<span class=\"emph alpha\">2015-02</span>)." +
-     "Submitted to JFR, Univerity of Bologna."
+     @("http://jfr.unibo.it/article/view/4716"
+     "Verified Representations of Landau's \"Grundlagen\" in the λδ Family and in the Calculus of Constructions") +
+     "(<span class=\"emph alpha\">2015-12</span>)." +
+     "In JFR 8(1), Univerity of Bologna, pp. 93-116." +
+     @@("documentation.html#bibtex" "BibTeX entry") ^ "."
      * }
    ]
 }