X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fwww%2Flambdadelta%2Fweb%2Fhome%2Fdocumentation_3.tbl;h=4522bea00a21982de3f425397b0d8d13d6beb3e5;hb=3ba665bba69c4505ab8fb7a9be661667c097a646;hp=4df01fc55267f86e75d7f11683acab5e6ea588ee;hpb=c211eb61218aa9b43dfd2baae45407f0aa87ca79;p=helm.git
diff --git a/helm/www/lambdadelta/web/home/documentation_3.tbl b/helm/www/lambdadelta/web/home/documentation_3.tbl
index 4df01fc55..4522bea00 100644
--- 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" "J3a." "" } {
"F. Guidi:" +
- @@("download/gda.pdf"
- "A Verified Translation of Landau's \"Grundlagen\" from Automath into a Pure Type System, via λδ") +
- "(2015-02)." +
- "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") +
+ "(2015-12)." +
+ "In JFR 8(1), Univerity of Bologna, pp. 93-116." +
+ @@("html/documentation.html#bibtex" "BibTeX entry") ^ "."
+ * }
+ ]
+ [ { name "ldR3a" "R3a." "" } {
+ "F. Guidi:" +
+ @("http://amsacta.unibo.it/5754/"
+ "The Formal System λΥP") +
+ "(2017-12)." +
+ "University of Bologna, technical report AMS Acta 5754" +
+ "(accepted 2018-01)." +
+ @@("html/documentation.html#bibtex" "BibTeX entry") ^ "."
+ * }
+ ]
+ [ { name "ldP3a" "P3a." "" } {
+ "F. Guidi:" +
+ @@("download/ld_talk_10s.pdf"
+ "Adding Schematic Abstraction to λP") +
+ "(2018-02)." +
+ "Presentation at University of Bologna (slides)."
* }
]
}