install-jed install-bib install-2 install-1 install-coq \
install-automath install-v install-matita \
-LDURL = http://lambdadelta.info/
+# LDURL = http://lambdadelta.info/
+LDURL = http://helm.cs.unibo.it/lambdadelta/
SITEDIR = html
ETCDIR = etc
% \lambda\delta version 2 (active) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-@comment{lambdadeltaR2d,
+@misc{lambdadeltaJ2a,
author="Ferruccio {Guidi}",
title="{Two Formal Systems of the $\lambda\delta$ Family Revised}",
- howpublished="CoRR identifier 1411.0154",
- year="2014",
+ howpublished="Preprint",
+ year="2019",
month="November",
- note="Preprint (available at $<$\url{http://lambdadelta.info/}$>$)"
+ note="CoRR identifier 1911.12749",
}
@misc{lambdadeltaV2b,
institution="University of Bologna",
address="Bologna, Italy",
year="2015",
- month="December"
+ month="December",
+ note="CoRR identifier 1411.0154"
}
@misc{lambdadeltaV2a,
publisher="ACM",
address="New York, NY, USA",
year="2009",
- month="November"
+ month="November",
+ note="CoRR identifier cs/0611040"
}
@incollection{lambdadeltaR1c,
% \lambda\delta version 2 (active) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-@comment{lambdadeltaR2d,
+@misc{lambdadeltaJ2a,
author="Ferruccio {Guidi}",
title="{Two Formal Systems of the $\lambda\delta$ Family Revised}",
- howpublished="CoRR identifier 1411.0154",
- year="2014",
+ howpublished="Preprint",
+ year="2019",
month="November",
- note="Preprint (available at $<$\url{http://lambdadelta.info/}$>$)"
+ note="CoRR identifier 1911.12749",
}
@misc{lambdadeltaV2b,
institution="University of Bologna",
address="Bologna, Italy",
year="2015",
- month="December"
+ month="December",
+ note="CoRR identifier 1411.0154"
}
@misc{lambdadeltaV2a,
publisher="ACM",
address="New York, NY, USA",
year="2009",
- month="November"
+ month="November",
+ note="CoRR identifier cs/0611040"
}
@incollection{lambdadeltaR1c,
<rlink to="download/lambdadelta.bib">lambdadelta.bib</rlink>,
<notice class="alpha" notice="view"/>
<rlink to="download/lambdadelta.txt">lambdadelta.txt</rlink>
- (revised <notice class="gamma" notice="2018-01"/>).
+ (revised <notice class="gamma" notice="2019-11"/>).
</body>
<subsection name="v3"><img logo="ld3"/>λδ version 3 (proposed)</subsection>
name "documentation_2"
table {
-(*
[ { name "ldJ2a" "<span class=\"emph alpha\">J2a.</span>" "" } {
"F. Guidi:" +
- @@("download/basic2a.pdf"
- "The Formal System λδ Revised, Stage A: Extending the Applicability Condition") +
- "(<span class=\"emph gamma\">2014-11</span>)." +
+ @("https://arxiv.org/abs/1911.12749"
+ "Two Formal Systems of the λδ Family Revised") +
+ "(<span class=\"emph gamma\">2019-11</span>)." +
"Preprint." + (* Submitted to ACM ToCL. *)
"CoRR identifier" +
- @("http://arxiv.org/abs/1411.0154" "1411.0154") +
- "[v2] (revised" +
- "<span class=\"emph gamma\">2015-03</span>)." +
+ @("https://arxiv.org/abs/1911.12749" "1911.12749") +
+ "[v1] (revised" +
+ "<span class=\"emph gamma\">2019-11</span>)." +
@@("html/documentation.html#bibtex" "BibTeX entry") ^ "."
* }
]
-*)
[ { name "ldR2c" "<span class=\"emph alpha\">R2c.</span>" "" } {
"F. Guidi:" +
@("http://amsacta.unibo.it/4411/"
"Extending the Applicability Condition in the Formal System λδ") +
"(<span class=\"emph gamma\">2015-03</span>)." +
"University of Bologna, technical report AMS Acta 4411." +
+ "CoRR identifier" +
+ @("http://arxiv.org/abs/1411.0154" "1411.0154") +
+ "[v3] (revised" +
+ "<span class=\"emph delta\">2019-11</span>)." +
@@("html/documentation.html#bibtex" "BibTeX entry") ^ "."
* }
]
<body>
The λδ family is developed within the
<link to="http://helm.cs.unibo.it/">Hypertextual Electronic Library of Mathematics (HELM)</link>
- as a set of machine-checked digital specifications.
+ as a set of machine-checked <rlink to="html/specification.html">digital specifications</rlink>.
</body>
+ <topitem name="current">
+ Current version:
+ <rlink to="download/lambdadelta_2B.tar.bz2">λδ-2B for for Matita 0.99.4</rlink>
+ (released: <notice class="gamma" notice="2019-11"/>).
+ <rlink to="html/documentation.html#ldJ2a">Documentation (J2a)</rlink>.
+ </topitem>
<body>
This is the family logo: <rlink to="images/crux_177.png">crux_177.png</rlink>
(revised <notice class="alpha" text="2012-09"/>).
<link to="https://it.wikipedia.org/wiki/Umineko_no_naku_koro_ni">Umineko no Naku Koro ni</link>.
</body>
+<!-- ===================================================================== -->
+
+ <section15 name="info">lambdadelta.info</section15>
+
+ <body>
+ <img logo="forward"/>
+ If this image is not visible, forwarding is out of order.
+ </body>
+
<footer/>
</page>
<rlink to="download/lambdadelta_2B.tar.bz2">lambdadelta_2B for Matita 0.99.4</rlink>
(revised <notice class="gamma" text="2019-11"/>).
Source scripts [Git revision: 2019-11-19 20:45:15].
- <rlink to="html/documentation.html#ldV2b">Documentation (V2b)</rlink>.
+ <rlink to="html/documentation.html#ldJ2a">Documentation (J2a)</rlink>.
</body>
</topitem>
<!-- logo support -->
+<xsl:template name="forward-logo">
+ <a href="http://lambdadelta.info/"><img class="icon32"
+ alt="[forwarded logo]"
+ title="forwarded logo"
+ src="http://lambdadelta.info/images/crux_32.png"
+ /></a>
+</xsl:template>
+
<xsl:template name="crux-logo">
- <a href="{$baseurl}"><img class="icon32"
+ <a href="{$baseurl}html/home.html"><img class="icon32"
alt="[\lambda\delta home]"
title="\lambda\delta home"
src="{$baseurl}images/crux_32.png"
<xsl:template name="img">
<xsl:choose>
+ <xsl:when test="@logo='forward'">
+ <xsl:call-template name="forward-logo"/>
+ </xsl:when>
<xsl:when test="@logo='crux'">
<xsl:call-template name="crux-logo"/>
</xsl:when>