]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/www/lambdadelta/web/home/home.ldw.xml
update in apps_2
[helm.git] / helm / www / lambdadelta / web / home / home.ldw.xml
index a7e9b670247ec2eb39bd9f57bafc19a2cd75071d..8e6135836d861a64fffbbf64e845257b950916ab 100644 (file)
    <section9 name="foreword">Foreword</section9>
    <body>
       The formal systems of the λδ (\lambda\delta) family are typed λ-calculi aiming to support
-      the foundational frameworks for Mathematics that require an underlying specification language
-      (for example the <link to="http://www.math.unipd.it/~maietti/">Minimalist Foundation</link>
-       and its predecessors).
+      the foundational frameworks for Mathematics that require an underlying specification language,
+      for example the
+      <link to="http://www.math.unipd.it/~maietti/">Minimalist Foundation (MF)</link>
+      and its predecessors.
    </body>
    <body>
       The λδ family is developed within the
-      <link to="http://helm.cs.unibo.it/">Hypertextual Electronic Library of Mathematics</link>
+      <link to="http://helm.cs.unibo.it/">Hypertextual Electronic Library of Mathematics (HELM)</link>
       as a set of machine-checked digital specifications.
    </body>
    <body>
       (revised <notice class="alpha" text="2012-09"/>).
    </body>
    <body>
-      <notice class="alpha" text="Notice for the user of Internet Explorer."/>
-      To view this site correctly, please select a font
+      <notice class="alpha" text="Notice:"/>
+      to view this site correctly, please select a font
       with <link to="http://www.unicode.org/">Unicode</link> support.
-      For example "Lucida Sans Unicode" (it should be already installed on your system).
-      To change the current font follow:
-      "Tools" menu → "Internet Options" entry → "General" tab → "Fonts" button.
    </body>
 
 <!-- ===================================================================== -->
       This is a list of publications citing λδ documentation.
    </body>
 
+   <topitem name="C10">
+      M. Weber:
+      <notice class="alpha">An extended type system with lambda-typed lambda-expressions</notice>
+      (2018). Technical report. Faculty of Computer Science, Technical University of Berlin.
+   </topitem>
+
+   <topitem name="C9">
+      M. Weber:
+      <notice class="alpha">An extended type system with lambda-typed lambda-expressions (extended version)</notice>
+      (2018). Technical report. Faculty of Computer Science, Technical University of Berlin.
+   </topitem>
+
+   <topitem name="C8">
+      M.E. Maietti, S. Maschio:
+      <notice class="alpha">An extensional Kleene realizability semantics for the Minimalist Foundation</notice>
+      (2015). In Leibniz International Proceedings in Informatics, 39, pp 162-186. Schloss Dagstuhl, Leibniz-Zentrum für Informatik.
+   </topitem>
+
    <topitem name="C7">
       C. Dunchev, F. Guidi, C. Sacerdoti Coen, E. Tassi:
       <notice class="alpha">ELPI: Fast, Embeddable, λProlog Interpreter</notice>