update in basic_2

[helm.git] / helm / www / lambdadelta / web / home / documentation_3.tbl

diff --git a/helm/www/lambdadelta/web/home/documentation_3.tbl b/helm/www/lambdadelta/web/home/documentation_3.tbl
index 4df01fc55267f86e75d7f11683acab5e6ea588ee..4522bea00a21982de3f425397b0d8d13d6beb3e5 100644 (file)
--- a/helm/www/lambdadelta/web/home/documentation_3.tbl
+++ b/helm/www/lambdadelta/web/home/documentation_3.tbl
@@ -3,11 +3,29 @@ name "documentation_3"
 table {
    [ { 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." +
-     @@("documentation.html#bibtex" "BibTeX entry") ^ "."
+     @("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." +
+     @@("html/documentation.html#bibtex" "BibTeX entry") ^ "."
+     * }
+   ]
+   [ { name "ldR3a" "<span class=\"emph alpha\">R3a.</span>" "" } {
+     "F. Guidi:" +
+     @("http://amsacta.unibo.it/5754/"
+     "The Formal System λΥP") +
+     "(<span class=\"emph alpha\">2017-12</span>)." +
+     "University of Bologna, technical report AMS Acta 5754" +
+     "(accepted <span class=\"emph alpha\">2018-01</span>)." +
+     @@("html/documentation.html#bibtex" "BibTeX entry") ^ "."
+     * }
+   ]
+   [ { name "ldP3a" "<span class=\"emph alpha\">P3a.</span>" "" } {
+     "F. Guidi:" + 
+     @@("download/ld_talk_10s.pdf"
+     "Adding Schematic Abstraction to λP") +
+     "(<span class=\"emph alpha\">2018-02</span>)." +
+     "Presentation at University of Bologna (slides)."
      * }
    ]
 }