X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fweb%2Fhome%2Fdocumentation_3.tbl;h=d5d17a5700146d08bf70e3b17b34543c9ee5a20b;hb=528f8ea107f689d07d060e1d31ba32bf65b4e6ba;hp=ec291e009dfa9b49ac0d3a1bcb72a42ee6813e19;hpb=67fede5f273328bf920ad609f15d4f2389493c5c;p=helm.git diff --git a/helm/www/lambdadelta/web/home/documentation_3.tbl b/helm/www/lambdadelta/web/home/documentation_3.tbl index ec291e009..d5d17a570 100644 --- a/helm/www/lambdadelta/web/home/documentation_3.tbl +++ b/helm/www/lambdadelta/web/home/documentation_3.tbl @@ -1,12 +1,23 @@ name "documentation_3" table { - [ { name "ldJ4" "J4." "" } { + [ { 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." + @("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") ^ "." * } ] }