<div class="spacer">
<img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="head2sn" id="">Character classes</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">This table shows how the first 45 positive integers
+
<div xmlns:ld="http://lambdadelta.info/" class="head2sn" id="">Character classes</div>
+
<div xmlns:ld="http://lambdadelta.info/" class="text">This table shows how the first 45 positive integers
are distributed in the four classes.
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
+
<div xmlns:ld="http://lambdadelta.info/" class="text">
<table cellpadding="4" cellspacing="0">
<tbody>
<tr>
</tbody>
</table>
</div>
-
- <div class="spacer">
+ <div class="spacer">
<img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
</div>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 24 Dec 2014 22:58:52 +0100</div>
-</body>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Mon, 05 Jan 2015 00:32:03 +0100</div>
+ </body>
</html>
XSLTDIR = xslt
XMLDIR = xml
SRCDIR = web/home
+LDDLDIR = web/lddl
XHTBLDIR = bin/xhtbl
-HTMLDIR = $(HOME)/public_html/lddl
+HTMLDIR = static/lddl
JEDDIR = $(HOME)/mps/jed
BIBDIR = $(HOME)/texmf/bibtex/bib
CONTRIBDIR = $(ETCDIR)/lambdadelta
RDIR = /projects/helm/public_html/lambdadelta
RHOMEDIR = $(REMOTE):$(RDIR)
RXMLDIR = $(RHOMEDIR)/xml
-RHTMLDIR = $(RHOMEDIR)/static/lddl
RDOWNDIR = $(RHOMEDIR)/download
+RHTMLDIR = /projects/helm/public_html/lambda-delta/static
SLS = helena.sl automath.sl
BIB = lambdadelta.bib
$(H)scp $^ $(RDOWNDIR)
$(H)ssh $(REMOTE) "cd $(RDIR) && tar -xjf download/lddl.tar.bz2"
-# $(H)scp -r $(XMLDIR) $(RXMLDIR)
-
test-html:
@$(MAKE) --no-print-directory $(XMLS:%.xml=%)
@echo " MAKE */*.ld"
$(H). $<
-install-html: $(ETCDIR)/make_html.sh
+install-html $(DOWNDIR)/static_lddl.tar.bz2: $(ETCDIR)/exclude.txt $(ETCDIR)/make_html.sh
@echo " INSTALL html"
- $(H)scp -r $(HTMLDIR)/* $(RHTMLDIR)
+ $(H)tar -cjf $(DOWNDIR)/static_lddl.tar.bz2 -C static -X $< lddl
+ $(H)scp $(DOWNDIR)/static_lddl.tar.bz2 $(RDOWNDIR)
+ $(H)ssh $(REMOTE) "cd $(RHTMLDIR) && tar -xjf ../../lambdadelta/download/static_lddl.tar.bz2
install-jed: $(SLS:%=$(JEDDIR)/%)
@echo " INSTALL $(SLS)"
%.ld:
@echo " XSLT $@"
+ $(H)mkdir -p $(LDDLDIR)/$(@D)
+ $(H)$(XSLT) $(XSLT_OUT) $(LDDLDIR)/$@.ldw.xml $(XSLT_XSL) $(XSLTDIR)/lddl.xsl $(XSLT_IN) $(XMLDIR)/$@.xml
$(H)mkdir -p $(HTMLDIR)/$(@D)
- $(H)$(XSLT) $(XSLT_OUT) $(HTMLDIR)/$@.html $(XSLT_XSL) $(XSLTDIR)/lddl.xsl $(XSLT_IN) $(XMLDIR)/$@.xml
-
-%.ldc:
- @echo " SKIP $@"
+ $(H)$(XSLT) $(XSLT_OUT) $(HTMLDIR)/$@.html $(XSLT_XSL) $(XSLTDIR)/ld_web.xsl $(XSLT_IN) $(LDDLDIR)/$@.ldw.xml
.PHONY: $(TAGS)
<div class="spacer">
<img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">
+
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
<td class="snnn capitalize italic green">
<br />
</td>
- <td class="ssns capitalize italic green">
+ <td class="snns capitalize italic green">
<a href="http://lambdadelta.info/implementation.html">implementation</a>
</td>
+ <td class="ssnn capitalize italic green">
+ <br />
+ </td>
</tr>
<tr>
<td class="snns capitalize sky">
<a href="http://lambdadelta.info/specification.html#v2">version 2</a>
</td>
<td class="snnn capitalize green">(<a href="http://lambdadelta.info/ground_2.html">background</a> - <a href="http://lambdadelta.info/basic_2.html">core</a> - <a href="http://lambdadelta.info/apps_2.html">applications</a>)</td>
- <td class="ssns capitalize green">
+ <td class="snns capitalize green">
<a href="http://lambdadelta.info/implementation.html#lddl">library</a>
</td>
+ <td class="ssnn capitalize green">(<a href="http://lambdadelta.info/static/lddl/">static LDDL directory</a>)</td>
</tr>
<tr>
<td class="snss capitalize sky">
<td class="snss capitalize green">
<a href="http://lambdadelta.info/specification.html#v1">version 1</a>
</td>
- <td class="snsn capitalize green">
- <br />
- </td>
- <td class="ssss capitalize green">
+ <td class="snsn capitalize green">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
+ <td class="snss capitalize green">
<a href="http://lambdadelta.info/implementation.html#helena">helena</a>
</td>
+ <td class="sssn capitalize green">
+ <br />
+ </td>
</tr>
</tbody>
</table>
</div>
-
- <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="contents">Contents of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
+ <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="contents">Contents of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">This specification comprises a collection of checked
+
<div xmlns:ld="http://lambdadelta.info/" class="text">This specification comprises a collection of checked
applications of λδ version 2.
In particular it contains the components below.
</div>
- <ul xmlns:ld="http://lambdadelta.info/" id="MLTT1">
+
<ul xmlns:ld="http://lambdadelta.info/" id="MLTT1">
<li>
- <span class="emph alpha">MLTT1.</span>
+ <span class="emph alpha">MLTT1.</span>
Martin-Löf's Type Theory with one universe
using λδ as theory of expressions.
</li>
</ul>
- <ul xmlns:ld="http://lambdadelta.info/" id="functional">
+
<ul xmlns:ld="http://lambdadelta.info/" id="functional">
<li>
- <span class="emph alpha">Functional.</span>
+ <span class="emph alpha">Functional.</span>
The validation algorithm for λδ as implemented in
<a href="http://lambdadelta.info/implementation.html#helena">Helena 0.8</a>.
</li>
</ul>
-
- <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="summary">Summary of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
+ <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="summary">Summary of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical acount of the specification's contents
+
<div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical acount of the specification's contents
and its timeline.
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
+
<div xmlns:ld="http://lambdadelta.info/" class="text">
<table cellpadding="4" cellspacing="0">
<tbody>
<tr>
</tbody>
</table>
</div>
- <ul xmlns:ld="http://lambdadelta.info/">
+
<ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph alpha">2012 February 24.</span>
The Applications directory is started.
</li>
</ul>
- <ul xmlns:ld="http://lambdadelta.info/">
+
<ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph alpha">2011 December 20.</span>
The Functional component is started
inside the specification of λδ version 2.
</li>
</ul>
- <ul xmlns:ld="http://lambdadelta.info/">
+
<ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph alpha">2011 December 12.</span>
The MLTT1 component is started.
</li>
</ul>
-
- <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="structure">Logical Structure of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
+ <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="structure">Logical Structure of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">This table reports the specification's components and their planes.
+
<div xmlns:ld="http://lambdadelta.info/" class="text">This table reports the specification's components and their planes.
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
+
<div xmlns:ld="http://lambdadelta.info/" class="text">
<table cellpadding="4" cellspacing="0">
<tbody>
<tr>
</tbody>
</table>
</div>
-
- <div class="spacer">
+ <div class="spacer">
<img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
</div>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 24 Dec 2014 22:58:52 +0100</div>
-</body>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Mon, 05 Jan 2015 00:32:03 +0100</div>
+ </body>
</html>
<div class="spacer">
<img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">
+
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
<td class="snnn capitalize italic green">
<br />
</td>
- <td class="ssns capitalize italic green">
+ <td class="snns capitalize italic green">
<a href="http://lambdadelta.info/implementation.html">implementation</a>
</td>
+ <td class="ssnn capitalize italic green">
+ <br />
+ </td>
</tr>
<tr>
<td class="snns capitalize sky">
<a href="http://lambdadelta.info/specification.html#v2">version 2</a>
</td>
<td class="snnn capitalize green">(<a href="http://lambdadelta.info/ground_2.html">background</a> - <a href="http://lambdadelta.info/basic_2.html">core</a> - <a href="http://lambdadelta.info/apps_2.html">applications</a>)</td>
- <td class="ssns capitalize green">
+ <td class="snns capitalize green">
<a href="http://lambdadelta.info/implementation.html#lddl">library</a>
</td>
+ <td class="ssnn capitalize green">(<a href="http://lambdadelta.info/static/lddl/">static LDDL directory</a>)</td>
</tr>
<tr>
<td class="snss capitalize sky">
<td class="snss capitalize green">
<a href="http://lambdadelta.info/specification.html#v1">version 1</a>
</td>
- <td class="snsn capitalize green">
- <br />
- </td>
- <td class="ssss capitalize green">
+ <td class="snsn capitalize green">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
+ <td class="snss capitalize green">
<a href="http://lambdadelta.info/implementation.html#helena">helena</a>
</td>
+ <td class="sssn capitalize green">
+ <br />
+ </td>
</tr>
</tbody>
</table>
</div>
-
-
- <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="summary">Summary of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
+ <!--
+ <section>System's Syntax and Behavior</section>
+ <body>This is a summary of the "block structure"
+ of the System's syntactic items and reductions.
+ </body>
+ <table name="basic_2_blk"/>
+ <body>* In terms only.
+ ** In terms and local environments only.
+ *** In global environments only.
+ **** Sort level k in terms only.
+ </body>
+-->
+ <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="summary">Summary of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical acount of the specification's contents
+
<div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical acount of the specification's contents
and its timeline.
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
+
<div xmlns:ld="http://lambdadelta.info/" class="text">
<table cellpadding="4" cellspacing="0">
<tbody>
<tr>
</tbody>
</table>
</div>
-
- <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="B">Stage "B"</div>
- <ul xmlns:ld="http://lambdadelta.info/">
+ <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="B">Stage "B"</div>
+ <ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph alpha">Ongoing.</span>
Context-sensitive subject equivalence
for native type assignment.
</li>
</ul>
-
- <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="A">Stage "A": "Extending the Applicability Condition"</div>
- <ul xmlns:ld="http://lambdadelta.info/">
+ <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="A">Stage "A": "Extending the Applicability Condition"</div>
+ <ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph gamma">2014 October 28.</span>
λδ version 2A is released.
</li>
</ul>
- <ul xmlns:ld="http://lambdadelta.info/">
+
<ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph beta">2014 September 9.</span>
Iterated static type assignment defined (more elegantly)
as a primitive notion.
</li>
</ul>
- <ul xmlns:ld="http://lambdadelta.info/">
+
<ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph beta">2014 June 18.</span>
Preservation of stratified native validity
for context-sensitive computation on terms.
</li>
</ul>
- <ul xmlns:ld="http://lambdadelta.info/">
+
<ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph alpha">2014 June 9.</span>
Strong qrst-normalization
for simply typed terms.
</li>
</ul>
- <ul xmlns:ld="http://lambdadelta.info/">
+
<ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph alpha">2014 April 16.</span>
Lazy equivalence on local environments
(anniversary milestone).
</li>
</ul>
- <ul xmlns:ld="http://lambdadelta.info/">
+
<ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph alpha">2014 January 20.</span>
Parametrized slicing of local environments
(one from basic_1, the other used in basic_2 till now).
</li>
</ul>
- <ul xmlns:ld="http://lambdadelta.info/">
+
<ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph alpha">2013 August 7.</span>
Passive support for global environments.
</li>
</ul>
- <ul xmlns:ld="http://lambdadelta.info/">
+
<ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph alpha">2013 July 27.</span>
Reaxiomatized β-reductum as in rt-reduction.
</li>
</ul>
- <ul xmlns:ld="http://lambdadelta.info/">
+
<ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph alpha">2013 July 20.</span>
Context-sensitive strong rt-normalization
for simply typed terms.
</li>
</ul>
- <ul xmlns:ld="http://lambdadelta.info/">
+
<ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph alpha">2013 April 16.</span>
Reaxiomatized substitution and reduction
(anniversary milestone).
</li>
</ul>
- <ul xmlns:ld="http://lambdadelta.info/">
+
<ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph alpha">2013 March 16.</span>
Mutual recursive preservation of stratified native validity
for rst-computation on closures.
</li>
</ul>
- <ul xmlns:ld="http://lambdadelta.info/">
+
<ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph alpha">2012 October 16.</span>
Confluence for context-free parallel reduction on closures.
</li>
</ul>
- <ul xmlns:ld="http://lambdadelta.info/">
+
<ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph alpha">2012 July 26.</span>
Term binders polarized to control ζ-reduction (not released).
</li>
</ul>
- <ul xmlns:ld="http://lambdadelta.info/">
+
<ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph alpha">2012 April 16.</span>
Context-sensitive subject equivalence
(anniversary milestone).
</li>
</ul>
- <ul xmlns:ld="http://lambdadelta.info/">
+
<ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph alpha">2012 March 15.</span>
Context-sensitive strong normalization
for simply typed terms.
</li>
</ul>
- <ul xmlns:ld="http://lambdadelta.info/">
+
<ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph alpha">2012 January 27.</span>
Support for abstract candidates of reducibility.
</li>
</ul>
- <ul xmlns:ld="http://lambdadelta.info/">
+
<ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph alpha">2011 September 21.</span>
Confluence for context-sensitive parallel reduction on terms.
</li>
</ul>
- <ul xmlns:ld="http://lambdadelta.info/">
+
<ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph alpha">2011 September 6.</span>
Confluence for context-free parallel reduction on terms.
</li>
</ul>
- <ul xmlns:ld="http://lambdadelta.info/">
+
<ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph alpha">2011 April 17.</span>
Specification starts.
</li>
</ul>
-
- <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="structure">Logical Structure of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
+ <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="structure">Logical Structure of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">This table reports the specification's components and their planes.
+
<div xmlns:ld="http://lambdadelta.info/" class="text">This table reports the specification's components and their planes.
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
+
<div xmlns:ld="http://lambdadelta.info/" class="text">
<table cellpadding="4" cellspacing="0">
<tbody>
<tr>
</tbody>
</table>
</div>
-
- <div class="spacer">
+ <div class="spacer">
<img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
</div>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 24 Dec 2014 22:58:52 +0100</div>
-</body>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Mon, 05 Jan 2015 00:32:03 +0100</div>
+ </body>
</html>
let msg = P.sprintf "This file was generated by %s, do not edit" myself
let compose uri ext =
+ if uri.[pred (S.length uri)] = '/' then uri else
try
let i = S.index uri '#' in
let uri, fragment = S.sub uri 0 i, S.sub uri i (S.length uri - i) in
a:link, a:visited, a:hover, a:active, a:focus {
text-decoration: underline;
- color: rgb(0, 0, 0);
+ color: inherit;
+ backgroud: inherit;
}
a:hover {
+ text-decoration: underline;
+ color: inherit;
background: rgb(192, 192, 192);
}
color: rgb(255, 0, 0);
}
+.proj {
+ background: rgb(255, 255, 255);
+ color: rgb(192, 120, 0);
+}
+
.local {
background: rgb(255, 255, 255);
color: rgb(0, 160, 0);
.global {
background: rgb(255, 255, 255);
- color: rgb(0, 0, 0);
+ color: rgb(0, 0, 255);
}
<div class="spacer">
<img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">
+
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
<td class="snnn capitalize italic green">
<br />
</td>
- <td class="ssns capitalize italic green">
+ <td class="snns capitalize italic green">
<a href="http://lambdadelta.info/implementation.html">implementation</a>
</td>
+ <td class="ssnn capitalize italic green">
+ <br />
+ </td>
</tr>
<tr>
<td class="snns capitalize sky">
<a href="http://lambdadelta.info/specification.html#v2">version 2</a>
</td>
<td class="snnn capitalize green">(<a href="http://lambdadelta.info/ground_2.html">background</a> - <a href="http://lambdadelta.info/basic_2.html">core</a> - <a href="http://lambdadelta.info/apps_2.html">applications</a>)</td>
- <td class="ssns capitalize green">
+ <td class="snns capitalize green">
<a href="http://lambdadelta.info/implementation.html#lddl">library</a>
</td>
+ <td class="ssnn capitalize green">(<a href="http://lambdadelta.info/static/lddl/">static LDDL directory</a>)</td>
</tr>
<tr>
<td class="snss capitalize sky">
<td class="snss capitalize green">
<a href="http://lambdadelta.info/specification.html#v1">version 1</a>
</td>
- <td class="snsn capitalize green">
- <br />
- </td>
- <td class="ssss capitalize green">
+ <td class="snsn capitalize green">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
+ <td class="snss capitalize green">
<a href="http://lambdadelta.info/implementation.html#helena">helena</a>
</td>
+ <td class="sssn capitalize green">
+ <br />
+ </td>
</tr>
</tbody>
</table>
</div>
-
- <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="bibtex">Documentation <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
+ <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="bibtex">Documentation <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
+
<div xmlns:ld="http://lambdadelta.info/" class="text">
BibTeX database of λδ documentation:
<span class="emph alpha">download</span>
<a href="http://lambdadelta.info/download/lambdadelta.bib">lambdadelta.bib</a>,
<a href="http://lambdadelta.info/download/lambdadelta.txt">lambdadelta.txt</a>
(revised <span class="emph gamma">2014-10</span>).
</div>
-
- <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="v2">
+ <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="v2">
<img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" /> λδ version 2 (active)</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
+
<div xmlns:ld="http://lambdadelta.info/" class="text">
The main source of information is <span class="emph alpha">J2</span>.
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
+
<div xmlns:ld="http://lambdadelta.info/" class="text">
<table cellpadding="4" cellspacing="0">
<tbody>
<tr>
</tbody>
</table>
</div>
-
- <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="v1">
+ <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="v1">
<img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b6.png" /> λδ version 1 (superseded)</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
+
<div xmlns:ld="http://lambdadelta.info/" class="text">
The main source of information is <span class="emph alpha">J1</span>.
A summary is available in <span class="emph alpha">P5</span>.
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
+
<div xmlns:ld="http://lambdadelta.info/" class="text">
<table cellpadding="4" cellspacing="0">
<tbody>
<tr>
</tbody>
</table>
</div>
-
- <div class="spacer">
+ <div class="spacer">
<img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
</div>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 24 Dec 2014 22:58:52 +0100</div>
-</body>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Mon, 05 Jan 2015 00:32:03 +0100</div>
+ </body>
</html>
<div class="spacer">
<img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">
+
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
<td class="snnn capitalize italic green">
<br />
</td>
- <td class="ssns capitalize italic green">
+ <td class="snns capitalize italic green">
<a href="http://lambdadelta.info/implementation.html">implementation</a>
</td>
+ <td class="ssnn capitalize italic green">
+ <br />
+ </td>
</tr>
<tr>
<td class="snns capitalize sky">
<a href="http://lambdadelta.info/specification.html#v2">version 2</a>
</td>
<td class="snnn capitalize green">(<a href="http://lambdadelta.info/ground_2.html">background</a> - <a href="http://lambdadelta.info/basic_2.html">core</a> - <a href="http://lambdadelta.info/apps_2.html">applications</a>)</td>
- <td class="ssns capitalize green">
+ <td class="snns capitalize green">
<a href="http://lambdadelta.info/implementation.html#lddl">library</a>
</td>
+ <td class="ssnn capitalize green">(<a href="http://lambdadelta.info/static/lddl/">static LDDL directory</a>)</td>
</tr>
<tr>
<td class="snss capitalize sky">
<td class="snss capitalize green">
<a href="http://lambdadelta.info/specification.html#v1">version 1</a>
</td>
- <td class="snsn capitalize green">
- <br />
- </td>
- <td class="ssss capitalize green">
+ <td class="snsn capitalize green">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
+ <td class="snss capitalize green">
<a href="http://lambdadelta.info/implementation.html#helena">helena</a>
</td>
+ <td class="sssn capitalize green">
+ <br />
+ </td>
</tr>
</tbody>
</table>
</div>
-
- <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="summary">Summary of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
+ <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="summary">Summary of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical acount of the specification's contents
+
<div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical acount of the specification's contents
and its timeline.
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
+
<div xmlns:ld="http://lambdadelta.info/" class="text">
<table cellpadding="4" cellspacing="0">
<tbody>
<tr>
</tbody>
</table>
</div>
- <ul xmlns:ld="http://lambdadelta.info/">
+
<ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph alpha">2013 November 27.</span>
Natural numbers with infinity.
</li>
</ul>
- <ul xmlns:ld="http://lambdadelta.info/">
+
<ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph alpha">2011 August 10.</span>
Specification starts.
</li>
</ul>
-
- <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="structure">Logical Structure of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
+ <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="structure">Logical Structure of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">This table reports the specification's components and their planes.
+
<div xmlns:ld="http://lambdadelta.info/" class="text">This table reports the specification's components and their planes.
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
+
<div xmlns:ld="http://lambdadelta.info/" class="text">
<table cellpadding="4" cellspacing="0">
<tbody>
<tr>
</tbody>
</table>
</div>
-
- <div class="spacer">
+ <div class="spacer">
<img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
</div>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 24 Dec 2014 22:58:52 +0100</div>
-</body>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Mon, 05 Jan 2015 00:32:03 +0100</div>
+ </body>
</html>
<div class="spacer">
<img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">
+
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
<td class="snnn capitalize italic green">
<br />
</td>
- <td class="ssns capitalize italic green">
+ <td class="snns capitalize italic green">
<a href="http://lambdadelta.info/implementation.html">implementation</a>
</td>
+ <td class="ssnn capitalize italic green">
+ <br />
+ </td>
</tr>
<tr>
<td class="snns capitalize sky">
<a href="http://lambdadelta.info/specification.html#v2">version 2</a>
</td>
<td class="snnn capitalize green">(<a href="http://lambdadelta.info/ground_2.html">background</a> - <a href="http://lambdadelta.info/basic_2.html">core</a> - <a href="http://lambdadelta.info/apps_2.html">applications</a>)</td>
- <td class="ssns capitalize green">
+ <td class="snns capitalize green">
<a href="http://lambdadelta.info/implementation.html#lddl">library</a>
</td>
+ <td class="ssnn capitalize green">(<a href="http://lambdadelta.info/static/lddl/">static LDDL directory</a>)</td>
</tr>
<tr>
<td class="snss capitalize sky">
<td class="snss capitalize green">
<a href="http://lambdadelta.info/specification.html#v1">version 1</a>
</td>
- <td class="snsn capitalize green">
- <br />
- </td>
- <td class="ssss capitalize green">
+ <td class="snsn capitalize green">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
+ <td class="snss capitalize green">
<a href="http://lambdadelta.info/implementation.html#helena">helena</a>
</td>
+ <td class="sssn capitalize green">
+ <br />
+ </td>
</tr>
</tbody>
</table>
</div>
-
- <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="tools">Tools <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b5.png" />
+ <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="tools">Tools <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b5.png" />
</div>
-
- <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="lddl">
+ <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="lddl">
<img class="icon32" alt="[Crux logo]" title="the Crux" src="http://lambdadelta.info/images/crux_32.png" /> λδ Digital Library (LDDL)</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
+
<div xmlns:ld="http://lambdadelta.info/" class="text">
The λδ Digital Library is part of <a href="http://helm.cs.unibo.it/">HELM</a>
and contains resources expressed in λδ.
</div>
- <ul xmlns:ld="http://lambdadelta.info/" id="contents">
+
<ul xmlns:ld="http://lambdadelta.info/" id="contents">
<li>
- <span class="emph alpha">Contents:</span>
+ <span class="emph alpha">Contents:</span>
Landau's "Grundlagen der Analysis"
(from Jutting's specification in <a href="http://www.win.tue.nl/automath/">Automath</a>).
</li>
</ul>
- <ul xmlns:ld="http://lambdadelta.info/" id="access">
+
<ul xmlns:ld="http://lambdadelta.info/" id="access">
<li>
- <span class="emph alpha">Access:</span>
- <a href="http://lambdadelta.info/static/lddl/">static pages</a> (updated <span class="emph beta">2012-10</span>),
+ <span class="emph alpha">Access:</span>
+ <a href="http://lambdadelta.info/static/lddl/">static pages</a> (updated <span class="emph gamma">2015-01</span>),
<a href="http://lambdadelta.info/download/lddl.tar.bz2">data set</a> (updated <span class="emph gamma">2014-12</span>),
<a href="http://lambdadelta.info/xml/">HELM server URL</a> (updated <span class="emph gamma">2014-12</span>).
</li>
</ul>
- <ul xmlns:ld="http://lambdadelta.info/" id="examples">
+
<ul xmlns:ld="http://lambdadelta.info/" id="examples">
<li>
- <span class="emph alpha">Examples:</span>
- <a href="http://lambdadelta.info/static/lddl/brg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
+ <span class="emph alpha">Examples:</span>
+ <a href="http://lambdadelta.info/static/lddl/Environment/grundlagen_2/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
Grundlagen's definition "t234"</a>
- (in "basic_rg" λδ),
- <a href="http://lambdadelta.info/static/lddl/crg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
- Grundlagen's definition "t234"</a>
- (in "complete_rg" λδ).
+ in λδ version 4.
</li>
</ul>
-
- <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="helena">
+ <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="helena">
<img class="icon32" alt="[Helena logo]" title="Helena" src="http://lambdadelta.info/images/helena_32.png" /> Helena</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
- Helena is a λδ processor,
+
<div xmlns:ld="http://lambdadelta.info/" class="text">
+ Helena is a processor for λδ,
implemented in <a href="http://caml.inria.fr/">Caml</a>
as a part of the <a href="http://helm.cs.unibo.it/">HELM</a> software,
meant for testing the stable features of the calculus as well as the unstable ones.
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
+
<div xmlns:ld="http://lambdadelta.info/" class="text">
The processor source code is available in the directory
<a href="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&path=%2Ftrunk%2Fhelm%2Fsoftware%2Fhelena%2F&rev=0&sc=0">/trunk/helm/software/helena/</a>
of the <a href="http://helm.cs.unibo.it/software/index.html">HELM Svn repository</a>.
The Svn revisions containing the stable versions of Helena are indicated next.
</div>
- <ul xmlns:ld="http://lambdadelta.info/" id="v2">
+
<ul xmlns:ld="http://lambdadelta.info/" id="v2">
<li>
- <span class="emph beta">Version 0.8.2.</span>
- In progress.
+ <span class="emph gamma">Version 0.8.2 (2014-12).</span>
+ Uses λδ "Version 3" with layer variables as core language.
+ Supports exportation to Grafite
+ (the specification language of <a href="http://matita.cs.unibo.it/">Matita</a>).
+ The overall validation speed of the "Grundlagen der Analysis"
+ increases of 34% with respect to version 0.8.1.
+ [Svn revision: 13005] (<a href="http://lambdadelta.info/download/helena_0.8.2.tar.gz">archived source code</a>)
<ul>
<li>
The specification of Landau's "Grundlagen der Analysis"
(revised <span class="emph gamma">2014-12</span>).
</li>
<li>
- <span class="emph gamma">2014-12.</span>
+ <span class="emph gamma">2014-12.</span>
The corrected specification of Landau's "Grundlagen der Analysis"
is successfully validated in λδ "Version 3".
</li>
</ul>
- </li>
+ </li>
</ul>
- <ul xmlns:ld="http://lambdadelta.info/" id="v1">
+
<ul xmlns:ld="http://lambdadelta.info/" id="v1">
<li>
- <span class="emph beta">Version 0.8.1 (2010-11).</span>
- Uses a subset of λδ "Version 4" as the intermediate language.
+ <span class="emph beta">Version 0.8.1 (2010-11).</span>
+ Uses a subset of λδ "Version 4" as intermediate language.
Features importation from ".hln" files containing λδ textual syntax.
The overall validation speed of the "Grundlagen der Analysis"
increases of 22% with respect to version 0.8.0.
(revised <span class="emph alpha">2010-11</span>).
</li>
<li>
- <span class="emph beta">2009-12.</span>
+ <span class="emph beta">2009-12.</span>
Helena appears in F. Wiedijk's
<a href="http://www.cs.ru.nl/%7Efreek/digimath/index.html#helena">
index of computer math systems</a>.
</li>
</ul>
- </li>
+ </li>
</ul>
- <ul xmlns:ld="http://lambdadelta.info/" id="v0">
+
<ul xmlns:ld="http://lambdadelta.info/" id="v0">
<li>
- <span class="emph beta">Version 0.8.0 (2009-09).</span>
+ <span class="emph beta">Version 0.8.0 (2009-09).</span>
Supports λδ "Version 2" with naive implementation of impredicative sort inclusion.
Features importation from <a href="http://www.win.tue.nl/automath/">Automath</a>
and exportation to <a href="http://www.w3.org/XML/">XML</a>.
(revised <span class="emph gamma">2008-07</span>).
</li>
<li>
- <span class="emph beta">2009-09.</span>
+ <span class="emph beta">2009-09.</span>
Jutting's specification of Landau's "Grundlagen der Analysis"
enters λδ Digital Library.
</li>
<li>
- <span class="emph beta">2009-06.</span>
+ <span class="emph beta">2009-06.</span>
Jutting's specification of Landau's "Grundlagen der Analysis"
is successfully processed, enabling sort inclusion.
</li>
</ul>
- </li>
+ </li>
</ul>
- <div class="spacer">
<img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
</div>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 26 Dec 2014 16:35:05 +0100</div>
-</body>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Mon, 05 Jan 2015 00:32:03 +0100</div>
+ </body>
</html>
<div class="spacer">
<img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">
+
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
<td class="snnn capitalize italic green">
<br />
</td>
- <td class="ssns capitalize italic green">
+ <td class="snns capitalize italic green">
<a href="http://lambdadelta.info/implementation.html">implementation</a>
</td>
+ <td class="ssnn capitalize italic green">
+ <br />
+ </td>
</tr>
<tr>
<td class="snns capitalize sky">
<a href="http://lambdadelta.info/specification.html#v2">version 2</a>
</td>
<td class="snnn capitalize green">(<a href="http://lambdadelta.info/ground_2.html">background</a> - <a href="http://lambdadelta.info/basic_2.html">core</a> - <a href="http://lambdadelta.info/apps_2.html">applications</a>)</td>
- <td class="ssns capitalize green">
+ <td class="snns capitalize green">
<a href="http://lambdadelta.info/implementation.html#lddl">library</a>
</td>
+ <td class="ssnn capitalize green">(<a href="http://lambdadelta.info/static/lddl/">static LDDL directory</a>)</td>
</tr>
<tr>
<td class="snss capitalize sky">
<td class="snss capitalize green">
<a href="http://lambdadelta.info/specification.html#v1">version 1</a>
</td>
- <td class="snsn capitalize green">
- <br />
- </td>
- <td class="ssss capitalize green">
+ <td class="snsn capitalize green">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
+ <td class="snss capitalize green">
<a href="http://lambdadelta.info/implementation.html#helena">helena</a>
</td>
+ <td class="sssn capitalize green">
+ <br />
+ </td>
</tr>
</tbody>
</table>
</div>
-
- <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="foreword">Foreword <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b9.png" />
+ <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="foreword">Foreword <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b9.png" />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
+
<div xmlns:ld="http://lambdadelta.info/" class="text">
The formal system λδ (\lambda\delta) is a typed λ-calculus aiming to support
the foundations of Mathematics that require an underlying specification language
(for example the <a href="http://www.math.unipd.it/~maietti/">Minimal Type Theory</a>
and its predecessors).
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
+
<div xmlns:ld="http://lambdadelta.info/" class="text">
λδ is developed in the context of the
<a href="http://helm.cs.unibo.it/">Hypertextual Electronic Library of Mathematics</a>
as a machine-checked digital specification
that is not the formal counterpart of previous informal material.
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
+
<div xmlns:ld="http://lambdadelta.info/" class="text">
This is the System logo: <a href="http://lambdadelta.info/images/crux_177.png">crux_177.png</a>
(revised <span class="emph alpha">2012-09</span>).
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
+
<div xmlns:ld="http://lambdadelta.info/" class="text">
<span class="emph alpha">Notice for the user of Internet Explorer.</span>
To view this site correctly, please select a font
with <a href="http://www.unicode.org/">Unicode</a> support.
To change the current font follow:
"Tools" menu → "Internet Options" entry → "General" tab → "Fonts" button.
</div>
-
-
-
- <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="citations">Citations <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b9.png" />
+ <!-- ===================================================================== -->
+ <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="citations">Citations <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b9.png" />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
+
<div xmlns:ld="http://lambdadelta.info/" class="text">
This is a list of publications citing λδ (not including our own).
</div>
-
- <ul xmlns:ld="http://lambdadelta.info/" id="C6">
+ <ul xmlns:ld="http://lambdadelta.info/" id="C6">
<li>
A. Asperti, W. Ricciotti, C. Sacerdoti Coen, E. Tassi:
<span class="emph alpha">Formal metatheory of programming languages in the Matita interactive theorem prover</span>
(2012). In JAR 49(3), pp. 427-451.
</li>
</ul>
-
- <ul xmlns:ld="http://lambdadelta.info/" id="C5">
+ <ul xmlns:ld="http://lambdadelta.info/" id="C5">
<li>
M.E. Maietti:
<span class="emph alpha">Consistency of the minimalist foundation with Church thesis and Bar Induction</span>
(2012). Submitted article.
</li>
</ul>
-
- <ul xmlns:ld="http://lambdadelta.info/" id="C4">
+ <ul xmlns:ld="http://lambdadelta.info/" id="C4">
<li>
W. Ricciotti:
<span class="emph alpha">Theoretical and implementation aspects in the mechanization of the metatheory of programming languages</span>
(July 2011). Ph.D. Thesis in Computer Science, Technical Report UBLCS-2011-09, University of Bologna.
</li>
</ul>
-
- <ul xmlns:ld="http://lambdadelta.info/" id="C3">
+ <ul xmlns:ld="http://lambdadelta.info/" id="C3">
<li>
C.E. Brown:
<span class="emph alpha">Faithful Reproductions of the Automath Landau Formalization</span>
(2011). Typescript note.
</li>
</ul>
-
- <ul xmlns:ld="http://lambdadelta.info/" id="C2">
+ <ul xmlns:ld="http://lambdadelta.info/" id="C2">
<li>
M.E. Maietti:
<span class="emph alpha">A minimalist two-level foundation for constructive mathematics</span>
(2009). In APAL 160(3), pp. 319-354.
</li>
</ul>
-
- <ul xmlns:ld="http://lambdadelta.info/" id="C1">
+ <ul xmlns:ld="http://lambdadelta.info/" id="C1">
<li>
V. Rahili:
<span class="emph alpha">First Year Report: Realisability methods of proof and semantics with application to expansion</span>
(July 2007). Typescript note.
</li>
</ul>
-
- <div class="spacer">
+ <div class="spacer">
<img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
</div>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 24 Dec 2014 22:58:52 +0100</div>
-</body>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Mon, 05 Jan 2015 00:32:03 +0100</div>
+ </body>
</html>
<div class="spacer">
<img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">
+
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
<td class="snnn capitalize italic green">
<br />
</td>
- <td class="ssns capitalize italic green">
+ <td class="snns capitalize italic green">
<a href="http://lambdadelta.info/implementation.html">implementation</a>
</td>
+ <td class="ssnn capitalize italic green">
+ <br />
+ </td>
</tr>
<tr>
<td class="snns capitalize sky">
<a href="http://lambdadelta.info/specification.html#v2">version 2</a>
</td>
<td class="snnn capitalize green">(<a href="http://lambdadelta.info/ground_2.html">background</a> - <a href="http://lambdadelta.info/basic_2.html">core</a> - <a href="http://lambdadelta.info/apps_2.html">applications</a>)</td>
- <td class="ssns capitalize green">
+ <td class="snns capitalize green">
<a href="http://lambdadelta.info/implementation.html#lddl">library</a>
</td>
+ <td class="ssnn capitalize green">(<a href="http://lambdadelta.info/static/lddl/">static LDDL directory</a>)</td>
</tr>
<tr>
<td class="snss capitalize sky">
<td class="snss capitalize green">
<a href="http://lambdadelta.info/specification.html#v1">version 1</a>
</td>
- <td class="snsn capitalize green">
- <br />
- </td>
- <td class="ssss capitalize green">
+ <td class="snsn capitalize green">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
+ <td class="snss capitalize green">
<a href="http://lambdadelta.info/implementation.html#helena">helena</a>
</td>
+ <td class="sssn capitalize green">
+ <br />
+ </td>
</tr>
</tbody>
</table>
</div>
-
-
-
- <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="milestones">Milestones <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b3.png" />
+ <!-- ===================================================================== -->
+ <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="milestones">Milestones <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b3.png" />
</div>
-
- <ul xmlns:ld="http://lambdadelta.info/">
+ <ul xmlns:ld="http://lambdadelta.info/">
+ <li>
+ <span class="emph gamma">December 2014.</span>
+ <a href="http://lambdadelta.info/implementation.html#v2">"Helena 0.8.2"</a> is released.
+ <ul>
+ <li>
+ The corrected specification of Landau's "Grundlagen der Analysis"
+ is validated in λδ version 3.
+ </li>
+ </ul>
+ </li>
+ </ul>
+ <ul xmlns:ld="http://lambdadelta.info/">
+ <li>
+ <span class="emph gamma">October 2014.</span>
+ <a href="http://lambdadelta.info/documentation.html#ldJ2">λδ version 2A</a>
+ is released.
+ </li>
+ </ul>
+ <ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph beta">July 2014.</span>
A new version of this site is online.
</li>
</ul>
-
- <ul xmlns:ld="http://lambdadelta.info/">
+ <ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph beta">June 2014.</span>
- <a href="http://lambdadelta.info/documentation.html#ldP8">First communication on λδ version 2.</a>
- </li>
+
<a href="http://lambdadelta.info/documentation.html#ldP8">First communication on λδ version 2.</a>
+ </li>
</ul>
-
- <ul xmlns:ld="http://lambdadelta.info/">
+ <ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph alpha">December 2012.</span>
The character "_" is removed from the denomination "lambda_delta":
(pointing at this site).
</li>
</ul>
- </li>
+ </li>
</ul>
-
- <ul xmlns:ld="http://lambdadelta.info/">
+ <ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph alpha">September 2011.</span>
The denomination "lambda-delta" changes to "lambda_delta":
In particular, this refactoring involves file names and path names.
</li>
</ul>
- </li>
+ </li>
</ul>
-
- <ul xmlns:ld="http://lambdadelta.info/">
+ <ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph alpha">April 2011.</span>
The specification of <a href="http://lambdadelta.info/version_2.html">λδ version 2</a>
<a href="http://matita.cs.unibo.it/">Matita 0.5</a>.
</li>
</ul>
-
- <ul xmlns:ld="http://lambdadelta.info/">
+ <ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph delta">February 2011.</span>
The specification of λδ version 2 with Coq 7.3.1 is abandoned.
</li>
</ul>
-
- <ul xmlns:ld="http://lambdadelta.info/">
+ <ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph alpha">December 2010.</span>
Transient λδ URL acquired: http://lambda-delta.info/ (expires on December 2012).
</li>
</ul>
-
- <ul xmlns:ld="http://lambdadelta.info/">
+ <ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph beta">November 2010.</span>
- "Helena 0.8.1" is released.
+ <a href="http://lambdadelta.info/implementation.html#v1">"Helena 0.8.1"</a> is released.
</li>
</ul>
-
- <ul xmlns:ld="http://lambdadelta.info/">
+ <ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph beta">September 2009.</span>
- "Helena 0.8.0" is released and the
- <a href="http://lambdadelta.info/implementation.html#lddl">λδ Digital Library</a>
- is started.
+ <a href="http://lambdadelta.info/implementation.html#v0">"Helena 0.8.0"</a> is released and the
+ <a href="http://lambdadelta.info/implementation.html#lddl">λδ Digital Library</a> is started.
</li>
</ul>
-
- <ul xmlns:ld="http://lambdadelta.info/">
+ <ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph alpha">June 2009.</span>
"Helena", a <a href="http://lambdadelta.info/implementation.html#helena">validator for λδ version 2</a>,
is available as a part of the <a href="http://helm.cs.unibo.it/">HELM</a> software.
</li>
</ul>
-
- <ul xmlns:ld="http://lambdadelta.info/">
+ <ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph alpha">September 2008.</span>
This site is online.
</li>
</ul>
-
- <ul xmlns:ld="http://lambdadelta.info/">
+ <ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph delta">July 2008.</span>
- <a href="http://lambdadelta.info/documentation.html#ldJ1">First journal paper on λδ</a>
+
<a href="http://lambdadelta.info/documentation.html#ldJ1">First journal paper on λδ</a>
accepted for publication.
</li>
</ul>
-
- <ul xmlns:ld="http://lambdadelta.info/">
+ <ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph delta">July 2008.</span>
First <a href="http://helm.cs.unibo.it/procedural/">procedural reconstruction</a>
of the λδ version 1 for Coq 7.3.1.
</li>
</ul>
-
- <ul xmlns:ld="http://lambdadelta.info/">
+ <ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph delta">June 2008.</span>
The <a href="http://lambdadelta.info/version_1.html#static">
are online.
</li>
</ul>
-
- <ul xmlns:ld="http://lambdadelta.info/">
+ <ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph delta">May 2008.</span>
The specification of λδ version 1 is concluded.
</li>
</ul>
-
- <ul xmlns:ld="http://lambdadelta.info/">
+ <ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph alpha">March 2008.</span>
The specification of λδ version 2 is started with Coq 7.3.1 (false start).
</li>
</ul>
-
- <ul xmlns:ld="http://lambdadelta.info/">
+ <ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph gamma">September 2007.</span>
The <a href="http://lambdadelta.info/version_1.html#dynamic">
is online.
</li>
</ul>
-
- <ul xmlns:ld="http://lambdadelta.info/">
+ <ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph gamma">November 2006.</span>
- <a href="http://lambdadelta.info/documentation.html#ldR2">λδ version 1</a>
+
<a href="http://lambdadelta.info/documentation.html#ldR2">λδ version 1</a>
is released.
</li>
</ul>
-
- <ul xmlns:ld="http://lambdadelta.info/">
+ <ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph beta">December 2005.</span>
- <a href="http://lambdadelta.info/documentation.html#ldP1">First communication on λδ version 1</a>.
+
<a href="http://lambdadelta.info/documentation.html#ldP1">First communication on λδ version 1</a>.
</li>
</ul>
-
- <ul xmlns:ld="http://lambdadelta.info/">
+ <ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph alpha">May 2004.</span>
The specification of <a href="http://lambdadelta.info/version_1.html">λδ version 1</a>
is started with Coq 7.3.1.
</li>
</ul>
-
-
-
- <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="visibility">Visibility <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b3.png" />
+ <!-- ===================================================================== -->
+ <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="visibility">Visibility <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b3.png" />
</div>
-
- <ul xmlns:ld="http://lambdadelta.info/">
+ <ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph alpha">June 2014.</span>
The <a href="http://www.google.com/">Google</a>
5 resources about λδ in the first 6 results.
</li>
</ul>
-
- <ul xmlns:ld="http://lambdadelta.info/">
+ <ul xmlns:ld="http://lambdadelta.info/">
<li>
<span class="emph alpha">June 2014.</span>
The <a href="http://www.yahoo.com/">Yahoo</a>
4 resources about λδ in the first 5 results.
</li>
</ul>
-
- <div class="spacer">
+ <div class="spacer">
<img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
</div>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 24 Dec 2014 22:58:51 +0100</div>
-</body>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Mon, 05 Jan 2015 00:32:03 +0100</div>
+ </body>
</html>
<div class="spacer">
<img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">
+
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
<td class="snnn capitalize italic green">
<br />
</td>
- <td class="ssns capitalize italic green">
+ <td class="snns capitalize italic green">
<a href="http://lambdadelta.info/implementation.html">implementation</a>
</td>
+ <td class="ssnn capitalize italic green">
+ <br />
+ </td>
</tr>
<tr>
<td class="snns capitalize sky">
<a href="http://lambdadelta.info/specification.html#v2">version 2</a>
</td>
<td class="snnn capitalize green">(<a href="http://lambdadelta.info/ground_2.html">background</a> - <a href="http://lambdadelta.info/basic_2.html">core</a> - <a href="http://lambdadelta.info/apps_2.html">applications</a>)</td>
- <td class="ssns capitalize green">
+ <td class="snns capitalize green">
<a href="http://lambdadelta.info/implementation.html#lddl">library</a>
</td>
+ <td class="ssnn capitalize green">(<a href="http://lambdadelta.info/static/lddl/">static LDDL directory</a>)</td>
</tr>
<tr>
<td class="snss capitalize sky">
<td class="snss capitalize green">
<a href="http://lambdadelta.info/specification.html#v1">version 1</a>
</td>
- <td class="snsn capitalize green">
- <br />
- </td>
- <td class="ssss capitalize green">
+ <td class="snsn capitalize green">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
+ <td class="snss capitalize green">
<a href="http://lambdadelta.info/implementation.html#helena">helena</a>
</td>
+ <td class="sssn capitalize green">
+ <br />
+ </td>
</tr>
</tbody>
</table>
</div>
-
- <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="specifications">Computer-checked formal specifications <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b5.png" />
+ <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="specifications">Computer-checked formal specifications <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b5.png" />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
+
<div xmlns:ld="http://lambdadelta.info/" class="text">
λδ is developed as a machine-checked digital specification.
It comes in several versions listed in the next table,
which includes the major milestones.
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
+
<div xmlns:ld="http://lambdadelta.info/" class="text">
The life cycle of a specification consists of four periods.
<span class="emph alpha">Alpha:</span>
the definitions are designed and the major propositions are proved,
<span class="emph delta">Delta:</span>
after its conclusion, the specification is modified just for maintenance.
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
+
<div xmlns:ld="http://lambdadelta.info/" class="text">
<table cellpadding="4" cellspacing="0">
<tbody>
<tr>
</tbody>
</table>
</div>
-
-
-
- <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="v2">
+ <!-- VERSION 2 =========================================================== -->
+ <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="v2">
<img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" /> λδ version 2 (active)</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
+
<div xmlns:ld="http://lambdadelta.info/" class="text">
The formal specification of λδ version 2
is available in the following formats:
</div>
-
- <ul xmlns:ld="http://lambdadelta.info/" id="source2">
+ <ul xmlns:ld="http://lambdadelta.info/" id="source2">
<li>
- <div class="text">
- <a href="http://lambdadelta.info/download/lambdadelta_2.tar.gz">lambdadelta_2 for Matita 0.99.2</a>
+
<a href="http://lambdadelta.info/download/lambdadelta_2.tar.gz">lambdadelta_2 for Matita 0.99.2</a>
(revised <span class="emph gamma">2014-10</span>).
Source scripts.
</div>
- <div class="text">
The scripts are grouped in directories, first by part, then by component.
</div>
- <div class="text">
- <span class="emph alpha">Notice:</span>
+ <span class="emph alpha">Notice:</span>
the scripts are checked by the latest version of Matita from
<a href="http://matita.cs.unibo.it/download.shtml">HELM Subversion repository</a>
at path <trunk/matita/>.
</div>
- </li>
+ </li>
</ul>
-
- <div xmlns:ld="http://lambdadelta.info/" class="text">
+ <div xmlns:ld="http://lambdadelta.info/" class="text">
Informational pages on the parts of the specification:
<a href="http://lambdadelta.info/ground_2.html">Background</a>,
<a href="http://lambdadelta.info/basic_2.html">Core</a>,
<a href="http://lambdadelta.info/apps_2.html">Applications</a>.
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
+
<div xmlns:ld="http://lambdadelta.info/" class="text">
<span class="emph alpha">Notice on numerical acounts:</span>
nodes are counted according to the "intrinsic complexity measure"
[F. Guidi: "Procedural Representation of CIC Proof Terms"
Journal of Automated Reasoning 44(1-2), Springer (February 2010), pp. 53-78].
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
+
<div xmlns:ld="http://lambdadelta.info/" class="text">
<span class="emph alpha">Notice on displayed logical structures:</span>
from the logical standpoint, the source scripts are grouped in "planes"
and these are grouped in "components";
the notation for the relations or functions
introduced in each script, is shown in parentheses (? are placeholders).
</div>
-
-
-
- <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="v1">
+ <!-- VERSION 1 =========================================================== -->
+ <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="v1">
<img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b6.png" /> λδ version 1 (superseded)</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
+
<div xmlns:ld="http://lambdadelta.info/" class="text">
The formal specification of λδ version 1
is available in the following formats:
</div>
-
- <ul xmlns:ld="http://lambdadelta.info/" id="source1">
+ <ul xmlns:ld="http://lambdadelta.info/" id="source1">
<li>
- <div class="text">
- <a href="http://lambdadelta.info/download/lambdadelta_1.tar.gz">lambdadelta_1 for Coq 7.3.1</a>
+
<a href="http://lambdadelta.info/download/lambdadelta_1.tar.gz">lambdadelta_1 for Coq 7.3.1</a>
(revised <span class="emph delta">2012-10</span>).
Source scripts.
- </div>
- <div class="text">
+ </div>
The scripts are grouped in directories, one for each part.
</div>
- </li>
+ </li>
</ul>
-
- <ul xmlns:ld="http://lambdadelta.info/" id="static1">
+ <ul xmlns:ld="http://lambdadelta.info/" id="static1">
<li>
- <a href="http://lambdadelta.info/static/matita/lambdadelta/">lambdadelta_1 for Matita 0.5</a>
+
<a href="http://lambdadelta.info/static/matita/lambdadelta/">lambdadelta_1 for Matita 0.5</a>
(revised <span class="emph delta">2011-09</span>).
Static HTML pages generated by the <a href="http://helm.cs.unibo.it/">HELM</a> rendering engine.
<ul>
<li>
- <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/pr3/pr3/pr3_confluence.con.html">
+
<a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/pr3/pr3/pr3_confluence.con.html">
Confluence of reduction</a>
(Church-Rosser property).
</li>
<li>
- <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/props/ty3_correct.con.html">
+
<a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/props/ty3_correct.con.html">
Correctness of types</a>.
</li>
<li>
- <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/props/ty3_unique.con.html">
+
<a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/props/ty3_unique.con.html">
Uniqueness of types up to conversion</a>.
</li>
<li>
- <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/pr3/ty3_sred_pr3.con.html">
+
<a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/pr3/ty3_sred_pr3.con.html">
Subject reduction of the type assignment</a>.
</li>
<li>
- <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/arity_props/ty3_sn3.con.html">
+
<a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/arity_props/ty3_sn3.con.html">
Strong normalization of the typed terms</a>.
</li>
<li>
- <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/dec/ty3_inference.con.html">
+
<a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/dec/ty3_inference.con.html">
Decidability of the type inference problem</a>.
</li>
</ul>
- </li>
+ </li>
</ul>
-
- <ul xmlns:ld="http://lambdadelta.info/" id="dynamic1">
+ <ul xmlns:ld="http://lambdadelta.info/" id="dynamic1">
<li>
- <a href="http://mowgli.cs.unibo.it:58080/apply?keys=RT&xmluri=http://helm.cs.unibo.it/helm//html/folder/index.html&prop.media-type=text/html&param.thmedia-type=text/html&param.thkeys=T1%2CT2%2CL%2CE&param.embedkeys=d_c%2CTC1%2CHC2%2CL&param.thencoding=UTF-8&prop.encoding=UTF-8&prop.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&param.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&param.encoding=UTF-8&param.media-type=text/html&param.keys=d_c%2CC1%2CHC2%2CL&profile=default&param.profile=default&param.CICURI=theory:/matita/lambdadelta/">
+
<a href="http://mowgli.cs.unibo.it:58080/apply?keys=RT&xmluri=http://helm.cs.unibo.it/helm//html/folder/index.html&prop.media-type=text/html&param.thmedia-type=text/html&param.thkeys=T1%2CT2%2CL%2CE&param.embedkeys=d_c%2CTC1%2CHC2%2CL&param.thencoding=UTF-8&prop.encoding=UTF-8&prop.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&param.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&param.encoding=UTF-8&param.media-type=text/html&param.keys=d_c%2CC1%2CHC2%2CL&profile=default&param.profile=default&param.CICURI=theory:/matita/lambdadelta/">
lambdadelta_1 for Matita 0.5</a>
(revised <span class="emph delta">2011-09</span>).
<a href="http://helm.cs.unibo.it/">HELM</a> directory.
<span class="emph alpha">Notice: the HELM rendering engine is offline.</span>
- </li>
+ </li>
</ul>
-
- <div class="spacer">
+ <div class="spacer">
<img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
</div>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 24 Dec 2014 22:58:52 +0100</div>
-</body>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Mon, 05 Jan 2015 00:32:03 +0100</div>
+ </body>
</html>
</topitem>
<topitem name="access">
<notice class="alpha" notice="Access:"/>
- <rlink to="static/lddl/">static pages</rlink> (updated <notice class="beta" notice="2012-10"/>),
+ <rlink to="static/lddl/">static pages</rlink> (updated <notice class="gamma" notice="2015-01"/>),
<rlink to="download/lddl.tar.bz2">data set</rlink> (updated <notice class="gamma" notice="2014-12"/>),
<rlink to="xml/">HELM server URL</rlink> (updated <notice class="gamma" notice="2014-12"/>).
</topitem>
<topitem name="examples">
<notice class="alpha" notice="Examples:"/>
- <rlink to="static/lddl/brg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
+ <rlink to="static/lddl/Environment/grundlagen_2/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
Grundlagen's definition "t234"</rlink>
- (in "basic_rg" λδ),
- <rlink to="static/lddl/crg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
- Grundlagen's definition "t234"</rlink>
- (in "complete_rg" λδ).
+ in λδ version 4.
</topitem>
<subsection name="helena"><helena-icon/>Helena</subsection>
<body>
- Helena is a λδ processor,
+ Helena is a processor for λδ,
implemented in <link to="http://caml.inria.fr/">Caml</link>
as a part of the <link to="http://helm.cs.unibo.it/">HELM</link> software,
meant for testing the stable features of the calculus as well as the unstable ones.
The Svn revisions containing the stable versions of Helena are indicated next.
</body>
<topitem name="v2">
- <notice class="beta" notice="Version 0.8.2."/>
- In progress.
+ <notice class="gamma" notice="Version 0.8.2 (2014-12)."/>
+ Uses λδ "Version 3" with layer variables as core language.
+ Supports exportation to Grafite
+ (the specification language of <link to="http://matita.cs.unibo.it/">Matita</link>).
+ The overall validation speed of the "Grundlagen der Analysis"
+ increases of 34% with respect to version 0.8.1.
+ [Svn revision: 13005] (<rlink to="download/helena_0.8.2.tar.gz">archived source code</rlink>)
<list><item>
The specification of Landau's "Grundlagen der Analysis"
for <link to="http://matita.cs.unibo.it/">Matita 0.99.2</link>:
</topitem>
<topitem name="v1">
<notice class="beta" notice="Version 0.8.1 (2010-11)."/>
- Uses a subset of λδ "Version 4" as the intermediate language.
+ Uses a subset of λδ "Version 4" as intermediate language.
Features importation from ".hln" files containing λδ textual syntax.
The overall validation speed of the "Grundlagen der Analysis"
increases of 22% with respect to version 0.8.0.
<section3 name="milestones">Milestones</section3>
+ <news class="gamma" date="December 2014.">
+ <rlink to="implementation.html#v2">"Helena 0.8.2"</rlink> is released.
+ <list><item>
+ The corrected specification of Landau's "Grundlagen der Analysis"
+ is validated in λδ version 3.
+ </item></list>
+ </news>
+
+ <news class="gamma" date="October 2014.">
+ <rlink to="documentation.html#ldJ2">λδ version 2A</rlink>
+ is released.
+ </news>
+
<news class="beta" date="July 2014.">
A new version of this site is online.
</news>
</news>
<news class="beta" date="November 2010.">
- "Helena 0.8.1" is released.
+ <rlink to="implementation.html#v1">"Helena 0.8.1"</rlink> is released.
</news>
<news class="beta" date="September 2009.">
- "Helena 0.8.0" is released and the
- <rlink to="implementation.html#lddl">λδ Digital Library</rlink>
- is started.
+ <rlink to="implementation.html#v0">"Helena 0.8.0"</rlink> is released and the
+ <rlink to="implementation.html#lddl">λδ Digital Library</rlink> is started.
</news>
<news class="alpha" date="June 2009.">
@@("basic_2" "core") + "-" +
@@("apps_2" "applications") ^ ")"
* ]
- [ @@("specification#v1" "version 1") * ]
+ [ @@("specification#v1" "version 1")
+ "(" ^ @@("static/matita/lambdadelta/" "static HELM directory") ^ ")"
+ * ]
}
class "green" {
[ @@"implementation" * ]
- [ @@("implementation#lddl" "library") * ]
+ [ @@("implementation#lddl" "library")
+ "(" ^ @@("static/lddl/" "static LDDL directory") ^ ")"
+ * ]
[ @@("implementation#helena" "helena") * ]
}
]
<xsl:param name="baseurl"/>
<xsl:param name="date"/>
+<xsl:strip-space elements="*"/>
+
<xsl:include href="xhtbl.xsl"/>
<xsl:include href="ld_web_library.xsl"/>
<xsl:include href="ld_web_root.xsl"/>
doctype-public="-//W3C//DTD XHTML 1.1//EN"
doctype-system="http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd"
encoding="UTF-8"
- indent="yes"
/>
</xsl:stylesheet>
</body></html>
</xsl:template>
+<xsl:template match="@*|node()">
+ <xsl:copy>
+ <xsl:apply-templates select="@*|node()"/>
+ </xsl:copy>
+</xsl:template>
+
</xsl:stylesheet>
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ -->
-<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
- xmlns="http://www.w3.org/1999/xhtml"
->
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform">
-<xsl:param name="baseurl"/>
+<xsl:strip-space elements="*"/>
<xsl:include href="lddl_library.xsl"/>
<xsl:include href="lddl_term.xsl"/>
-<xsl:include href="lddl_entity.xsl"/>
+<xsl:include href="lddl_constant.xsl"/>
<xsl:include href="lddl_root.xsl"/>
<xsl:output
method="xml"
- doctype-public="-//W3C//DTD XHTML 1.1//EN"
- doctype-system="http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd"
encoding="UTF-8"
- indent="no"
/>
</xsl:stylesheet>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<!--
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ -->
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+ xmlns:ld="http://lambdadelta.info/"
+ xmlns="http://lambdadelta.info/"
+>
+
+<xsl:template name="CONSTANT">
+ <xsl:param name="kind"/>
+ <section5 name="constant">Constant</section5>
+ <subsection name="{$kind}">
+ <xsl:value-of select="$kind"/>
+ <xsl:call-template name="cn"/>
+ <xsl:call-template name="sp"/>
+ <xsl:call-template name="global"/>
+ <xsl:call-template name="sp"/>
+ <xsl:call-template name="op"/>
+ <xsl:call-template name="mk_path"/>
+ <xsl:call-template name="cp"/>
+ </subsection>
+ <body>
+ <xsl:call-template name="idescr"/>
+ <xsl:call-template name="qt"/>
+ <xsl:value-of select="@meta"/>
+ <xsl:call-template name="qt"/>
+ </body>
+ <body>
+ <xsl:apply-templates select="*"/>
+ </body>
+</xsl:template>
+
+<xsl:template match="ld:GDec">
+ <xsl:call-template name="CONSTANT">
+ <xsl:with-param name="kind">Declaration</xsl:with-param>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="ld:GDef">
+ <xsl:call-template name="CONSTANT">
+ <xsl:with-param name="kind">Definition</xsl:with-param>
+ </xsl:call-template>
+</xsl:template>
+
+</xsl:stylesheet>
+++ /dev/null
-<?xml version="1.0" encoding="UTF-8"?>
-
-<!--
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department, University of Bologna, Italy.
- ||I||
- ||T|| HELM is free software; you can redistribute it and/or
- ||A|| modify it under the terms of the GNU General Public License
- \ / version 2 or (at your option) any later version.
- \ / This software is distributed as is, NO WARRANTY.
- V_______________________________________________________________ -->
-
-<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
- xmlns:ld="http://lambdadelta.info/"
- xmlns="http://www.w3.org/1999/xhtml"
->
-
-<xsl:strip-space elements="ABST ABBR"/>
-
-<xsl:template name="ENTITY">
- <xsl:param name="kind"/>
- <div class="head2">
- <span class="global">
- <xsl:value-of select="$kind"/>
- <xsl:call-template name="cn"/>
- <xsl:call-template name="sp"/>
- <span class="gref">
- <xsl:call-template name="global"/>
- </span>
- <xsl:call-template name="sp"/>
- <xsl:call-template name="op"/>
- <span class="gref">
- <xsl:call-template name="mk_path"/>
- </span>
- <xsl:call-template name="cp"/>
- </span>
- </div>
- <div class="text">
- <xsl:call-template name="idescr"/>
- <xsl:call-template name="qt"/>
- <xsl:value-of select="@meta"/>
- <xsl:call-template name="qt"/>
- </div>
- <div class="text">
- <xsl:apply-templates/>
- </div>
-</xsl:template>
-
-<xsl:template match="ld:ABST">
- <xsl:call-template name="ENTITY">
- <xsl:with-param name="kind">Declaration</xsl:with-param>
- </xsl:call-template>
-</xsl:template>
-
-<xsl:template match="ld:ABBR">
- <xsl:call-template name="ENTITY">
- <xsl:with-param name="kind">Definition</xsl:with-param>
- </xsl:call-template>
-</xsl:template>
-
-</xsl:stylesheet>
V_______________________________________________________________ -->
<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
- xmlns:ld="http://lambdadelta.info/"
- xmlns="http://www.w3.org/1999/xhtml"
+ xmlns="http://lambdadelta.info/"
+ xmlns:xhtml="http://www.w3.org/1999/xhtml"
>
<xsl:template name="sp">
<xsl:text> </xsl:text>
</xsl:template>
-<xsl:template name="cm">
- <xsl:text>, </xsl:text>
-</xsl:template>
-
<xsl:template name="sl">
<xsl:text>/</xsl:text>
</xsl:template>
-<xsl:template name="plus">
- <xsl:text>+</xsl:text>
-</xsl:template>
-
<xsl:template name="fs">
<xsl:text>.​</xsl:text>
</xsl:template>
<xsl:text>]</xsl:text>
</xsl:template>
+<xsl:template name="oc">
+ <xsl:text>{</xsl:text>
+</xsl:template>
+
+<xsl:template name="cc">
+ <xsl:text>}</xsl:text>
+</xsl:template>
+
<xsl:template name="oa">
<xsl:text><</xsl:text>
</xsl:template>
<xsl:text>></xsl:text>
</xsl:template>
+<xsl:template name="us">
+ <xsl:text>_</xsl:text>
+</xsl:template>
+
<xsl:template name="cn">
<xsl:text>:</xsl:text>
</xsl:template>
<xsl:text>=</xsl:text>
</xsl:template>
-<xsl:template name="qt">
- <xsl:text>"</xsl:text>
+<xsl:template name="infinity">
+ <xsl:text>∞</xsl:text>
</xsl:template>
-<xsl:template name="idescr">
- <xsl:text>Informal description: </xsl:text>
+<xsl:template name="lambda">
+ <xsl:text>λ</xsl:text>
</xsl:template>
-<xsl:template name="vpars">
- <xsl:text>Validation parameters: </xsl:text>
+<xsl:template name="Pi">
+ <xsl:text>Π</xsl:text>
</xsl:template>
-<xsl:template name="shier">
- <xsl:text>sort hierarchy = </xsl:text>
+<xsl:template name="forall">
+ <xsl:text>∀</xsl:text>
</xsl:template>
-<xsl:template name="kopts">
- <xsl:text>kernel options = </xsl:text>
+<xsl:template name="delta">
+ <xsl:text>δ</xsl:text>
</xsl:template>
-<xsl:template name="multiple">
- <span class="separator">
- <xsl:call-template name="cm"/>
- </span>
+<xsl:template name="chi">
+ <xsl:text>χ</xsl:text>
</xsl:template>
-<xsl:template name="lambda">
- <a title="{@mark}">
- <xsl:choose>
- <xsl:when test="@level=0">
- <xsl:text disable-output-escaping="yes">&Pi;</xsl:text>
- <sup><xsl:value-of select="@level"/></sup>
- </xsl:when>
- <xsl:when test="@level=1">
- <xsl:text disable-output-escaping="yes">&Pi;</xsl:text>
- </xsl:when>
- <xsl:when test="@level=2">
- <xsl:text disable-output-escaping="yes">&lambda;</xsl:text>
- </xsl:when>
- <xsl:when test="not(@level)">
- <xsl:text disable-output-escaping="yes">&lambda;</xsl:text>
- <sup><xsl:text disable-output-escaping="yes">&infin;</xsl:text></sup>
- </xsl:when>
- <xsl:otherwise>
- <xsl:text disable-output-escaping="yes">&lambda;</xsl:text>
- <sup><xsl:value-of select="@level"/></sup>
- </xsl:otherwise>
- </xsl:choose>
- </a>
+<xsl:template name="cm">
+ <xsl:text>, </xsl:text>
</xsl:template>
-<xsl:template name="delta">
- <a title="{@mark}">
- <xsl:text disable-output-escaping="yes">&delta;</xsl:text>
- </a>
+<xsl:template name="qt">
+ <xsl:text>"</xsl:text>
</xsl:template>
-<xsl:template name="chi">
- <a title="{@mark}">
- <xsl:text disable-output-escaping="yes">&chi;</xsl:text>
- </a>
+<xsl:template name="idescr">
+ <xsl:text>Informal description: </xsl:text>
</xsl:template>
-<xsl:template name="position">
- <xsl:variable name="index">
- <xsl:value-of select="@position"/>
- <xsl:if test="@offset != 0">
- <xsl:call-template name="plus"/>
- <xsl:value-of select="@offset"/>
- </xsl:if>
- </xsl:variable>
- <a title="{$index}">
- <xsl:value-of select="@name"/>
- </a>
+<xsl:template name="vpars">
+ <xsl:text>Validation parameters: </xsl:text>
</xsl:template>
-<xsl:template name="lddlbaseurl">
- <xsl:value-of select="$baseurl"/>
- <xsl:value-of select="'static/lddl'"/>
+<xsl:template name="shier">
+ <xsl:text>sort hierarchy = </xsl:text>
</xsl:template>
-<xsl:template name="uri">
- <xsl:variable name="url">
- <xsl:call-template name="lddlbaseurl">
- <xsl:value-of select="substring-after(@uri,'ld:')"/>
- <xsl:text>.html</xsl:text>
- </xsl:variable>
- <a href="{$url}" title="{@uri}"><xsl:value-of select="@name"/></a>
+<xsl:template name="kopts">
+ <xsl:text>kernel options = </xsl:text>
</xsl:template>
<xsl:template name="global">
- <a title="{@mark}">
+ <xhtml:span class="global" title="{@position}">
<xsl:value-of select="@name"/>
- </a>
-</xsl:template>
-
-<xsl:template name="mk_names">
- <xsl:param name="names">
- <xsl:value-of select="normalize-space(@name)"/>
- <xsl:call-template name="sp"/>
- </xsl:param>
- <xsl:param name="sep" select="false()"/>
- <xsl:if test="$names and $sep">
- <xsl:call-template name="multiple"/>
- </xsl:if>
- <xsl:if test="$names">
- <span class="lref">
- <xsl:value-of select="substring-before($names, ' ')"/>
- </span>
- <xsl:call-template name="mk_names">
- <xsl:with-param name="names" select="substring-after($names, ' ')"/>
- <xsl:with-param name="sep" select="true()"/>
- </xsl:call-template>
- </xsl:if>
-</xsl:template>
-
-<xsl:template name="mk_terms">
- <xsl:for-each select="*">
- <xsl:apply-templates select="."/>
- <xsl:if test="(name()='Sort' or name()='LRef' or name()='GRef') and position()!=last()">
- <xsl:call-template name="multiple"/>
- </xsl:if>
- </xsl:for-each>
+ </xhtml:span>
</xsl:template>
-<xsl:template name="mk_binder">
- <xsl:param name="sep-seq"/>
- <xsl:call-template name="ob"/>
- <xsl:call-template name="mk_binder_rec1">
- <xsl:with-param name="sep-seq" select="$sep-seq"/>
- </xsl:call-template>
- <xsl:call-template name="cb"/>
-</xsl:template>
-
-<xsl:template name="mk_binder_rec1">
- <xsl:param name="sep-seq"/>
- <xsl:param name="names">
- <xsl:value-of select="normalize-space(@name)"/>
- <xsl:call-template name="sp"/>
- </xsl:param>
- <xsl:param name="sep" select="false()"/>
- <xsl:param name="start" select="true()"/>
- <xsl:param name="pos" select="1"/>
- <xsl:choose>
- <xsl:when test="$start and $pos <= count(*)">
- <xsl:if test="$names and $sep">
- <xsl:call-template name="multiple"/>
- </xsl:if>
- <span class="lref">
- <xsl:value-of select="substring-before($names, ' ')"/>
- </span>
- <xsl:copy-of select="$sep-seq"/>
- <xsl:call-template name="mk_binder_rec2">
- <xsl:with-param name="names" select="substring-after($names, ' ')"/>
- <xsl:with-param name="pos" select="$pos"/>
- <xsl:with-param name="sep-seq" select="$sep-seq"/>
- </xsl:call-template>
- </xsl:when>
- <xsl:when test="not($start) and $pos <= count(*)">
- <xsl:call-template name="mk_binder_rec2">
- <xsl:with-param name="names" select="$names"/>
- <xsl:with-param name="pos" select="$pos"/>
- <xsl:with-param name="sep-seq" select="$sep-seq"/>
- </xsl:call-template>
- </xsl:when>
- </xsl:choose>
-</xsl:template>
-
-<xsl:template name="mk_binder_rec2">
- <xsl:param name="sep-seq"/>
- <xsl:param name="names"/>
- <xsl:param name="pos"/>
- <xsl:apply-templates select="*[$pos]"/>
- <xsl:call-template name="mk_binder_rec1">
- <xsl:with-param name="sep-seq" select="$sep-seq"/>
- <xsl:with-param name="names" select="$names"/>
- <xsl:with-param name="sep" select="true()"/>
- <xsl:with-param name="start" select="name(*[$pos])='Sort' or name(*[$pos])='LRef' or name(*[$pos])='GRef'"/>
- <xsl:with-param name="pos" select="$pos+1"/>
- </xsl:call-template>
+<xsl:template name="lddlurl">
+ <xsl:value-of select="'static/lddl'"/>
</xsl:template>
<xsl:template name="mk_segment">
<xsl:param name="path"/>
<xsl:param name="name"/>
<xsl:variable name="url">
- <xsl:call-template name="lddlbaseurl">
+ <xsl:call-template name="lddlurl"/>
<xsl:value-of select="substring-after($path,'ld:')"/>
</xsl:variable>
- <a href="{$url}"><xsl:value-of select="$name"/></a>
+ <rlink to="{$url}"><xsl:value-of select="$name"/></rlink>
<xsl:call-template name="sl"/>
</xsl:template>
</xsl:when>
<xsl:otherwise>
<xsl:variable name="path" select="substring-before(@uri,$rpath)"/>
- <xsl:value-of select="substring-after(@uri,$path)"/>
+ <xhtml:span class="global">
+ <xsl:value-of select="substring-after(@uri,$path)"/>
+ </xhtml:span>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<xsl:template name="uri">
+ <xsl:variable name="url">
+ <xsl:call-template name="lddlurl"/>
+ <xsl:value-of select="substring-after(@uri,'ld:')"/>
+ <xsl:text>.html</xsl:text>
+ </xsl:variable>
+ <rlink to="{$url}"><xsl:value-of select="@name"/></rlink>
+</xsl:template>
+
+<xsl:template name="layer">
+ <xhtml:sup>
+ <xsl:choose>
+ <xsl:when test="@layer">
+ <xsl:value-of select="@layer"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="infinity"/>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xhtml:sup>
+</xsl:template>
+
+<xsl:template name="abst">
+ <xsl:choose>
+ <xsl:when test="@layer=0 and @position=1">
+ <xsl:call-template name="forall"/>
+ <xsl:call-template name="layer"/>
+ </xsl:when>
+ <xsl:when test="@layer=0">
+ <xsl:call-template name="Pi"/>
+ <xsl:call-template name="layer"/>
+ </xsl:when>
+ <xsl:when test="@layer=1 and @position=1">
+ <xsl:call-template name="forall"/>
+ </xsl:when>
+ <xsl:when test="@layer=1">
+ <xsl:call-template name="Pi"/>
+ </xsl:when>
+ <xsl:when test="@layer=2">
+ <xsl:call-template name="lambda"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="lambda"/>
+ <xsl:call-template name="layer"/>
</xsl:otherwise>
</xsl:choose>
</xsl:template>
-<xsl:template name="lddl">
- <xsl:text disable-output-escaping="yes">&lambda;&delta; Digital Library (LDDL)</xsl:text>
+<xsl:template name="abbr">
+ <xsl:call-template name="delta"/>
+</xsl:template>
+
+<xsl:template name="void">
+ <xsl:call-template name="chi"/>
</xsl:template>
+<xsl:template name="name">
+ <xsl:choose>
+ <xsl:when test="@name">
+ <xsl:value-of select="@name"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="us"/>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<xsl:template name="separator">
+
+<!--
+ <xsl:variable name="pos">
+ <xsl:value-of select="position()"/>
+ </xsl:variable>
+ <xsl:variable name="last">
+ <xsl:value-of select="last()"/>
+ </xsl:variable>
+ <xhtml:span class="separator" title="{$pos} {$last}">
+ <xsl:call-template name="fs"/>
+ </xhtml:span>
+-->
+ <xsl:choose>
+ <xsl:when test="last()>position()">
+ <xhtml:span class="separator">
+ <xsl:call-template name="fs"/>
+ </xhtml:span>
+ </xsl:when>
+ </xsl:choose>
+</xsl:template>
+
+<!--
+
+<xsl:template name="multiple">
+ <xhtml:span class="separator">
+ <xsl:call-template name="cm"/>
+ </xhtml:span>
+</xsl:template>
+
+<xsl:template name="mk_terms">
+ <xsl:for-each select="*">
+ <xsl:apply-templates select="."/>
+ <xsl:if test="(name()='Sort' or name()='LRef' or name()='GRef') and position()!=last()">
+ <xsl:call-template name="multiple"/>
+ </xsl:if>
+ </xsl:for-each>
+</xsl:template>
+
+-->
+
</xsl:stylesheet>
<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
xmlns:ld="http://lambdadelta.info/"
- xmlns="http://www.w3.org/1999/xhtml"
+ xmlns="http://lambdadelta.info/"
>
-<xsl:strip-space elements="ENTITY"/>
-
<xsl:template match="/">
- <html xmlns="http://www.w3.org/1999/xhtml" dir="ltr" lang="en-us"><head>
- <meta http-equiv="Content-Language" content="en-us"/>
- <meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/>
- <meta http-equiv="Content-Style-Type" content="text/css"/>
- <meta name="author" content="Ferruccio Guidi"/>
- <meta name="description" content="λδ digital library"/>
- <title>λδ digital library (LDDL)</title>
- <link rel="stylesheet" type="text/css"
- href="http://lambdadelta.info/css/ld_web.css"
- />
- <link rel="stylesheet" type="text/css"
- href="http://lambdadelta.info/css/lddl.css"
- />
- <link rel="shortcut icon"
- href="http://lambdadelta.info/images/crux_16.ico"
- />
- </head><body>
- <div class="spacer">
- <a href="http://lambdadelta.info/">
- <img class="icon32"
- alt="[λδ home]" title="λδ home"
- src="http://lambdadelta.info/images/crux_32.png"
- /></a>
- </div>
- <div class="head1">
- <xsl:call-template name="lddl"/>
- </div>
- <div class="spacer">
- <img class="rule"
- alt="[Spacer]" title="λδ rainbow rule"
- src="http://lambdadelta.info/images/rainbow.png"
- />
- </div>
- <xsl:apply-templates/>
- <div class="spacer">
- <a href="http://validator.w3.org/check?uri=referer">
- <img class="w3c"
- alt="[Valid XHTML 1.1]"
- title="Valid XHTML 1.1"
- src="http://www.w3.org/Icons/valid-xhtml11-blue"
- /></a>
- <a href="http://jigsaw.w3.org/css-validator/check/referer">
- <img class="w3c"
- alt="[Valid CSS level 2]"
- title="Valid CSS level 2"
- src="http://www.w3.org/Icons/valid-css2-blue"
- /></a>
- <a href="http://www.w3.org/XML/">
- <img class="w3c"
- alt="[Generated from XML via XSL]"
- title="Generated from XML via XSL"
- src="http://lambdadelta.info/images/xml_xsl2.png"
- /></a>
- <a href="http://lambdadelta.info/implementation.html#helena">
- <img class="w3c"
- alt="[Powered by Helena λδ processor]"
- title="Powered by Helena λδ processor"
- src="http://lambdadelta.info/images/helena_label.png"
- /></a>
- <a href="http://www.w3.org/Graphics/PNG/">
- <img class="w3c"
- alt="[PNG used here]"
- title="PNG used here"
- src="http://lambdadelta.info/images/PNGnow2.png"
- /></a>
- <a href="http://www.anybrowser.org/campaign/">
- <img class="w3c"
- alt="[Viewable with any browser]"
- title="Viewable with any browser"
- src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png"
- /></a>
- </div>
- </body></html>
+ <page description = "\lambda\delta home page"
+ title = "\lambda\delta home page"
+ head = "λδ digital library (LDDL)"
+ >
+ <sitemap name="sitemap"/>
+ <xsl:apply-templates select="*"/>
+ <footer><helena-label/></footer>
+ </page>
</xsl:template>
-<xsl:template match="ld:ENTITY">
- <xsl:apply-templates/>
- <div class="text">
+<xsl:template match="ld:CONSTANT">
+ <xsl:apply-templates select="*"/>
+ <body>
<xsl:call-template name="vpars"/>
<xsl:call-template name="shier"/>
<xsl:call-template name="qt"/>
<xsl:call-template name="qt"/>
<xsl:value-of select="@options"/>
<xsl:call-template name="qt"/>
- </div>
+ </body>
+</xsl:template>
+
+<xsl:template match="@*|node()">
+ <xsl:copy>
+ <xsl:apply-templates select="@*|node()"/>
+ </xsl:copy>
</xsl:template>
</xsl:stylesheet>
<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
xmlns:ld="http://lambdadelta.info/"
- xmlns="http://www.w3.org/1999/xhtml"
+ xmlns:xhtml="http://www.w3.org/1999/xhtml"
>
-<xsl:strip-space elements="Sort LRef GRef Cast Appl Abst Abbr Void"/>
-
-<xsl:template name="separator">
- <span class="separator">
- <xsl:call-template name="fs"/>
- </span>
-</xsl:template>
-
<xsl:template match="ld:Sort">
- <span class="sort">
- <xsl:call-template name="position"/>
- </span>
+ <xhtml:span class="sort" title="{@position}">
+ <xsl:value-of select="@name"/>
+ </xhtml:span>
</xsl:template>
<xsl:template match="ld:LRef">
- <span class="lref">
- <xsl:call-template name="position"/>
- </span>
+ <xhtml:span class="lref" title="{@position}">
+ <xsl:value-of select="@name"/>
+ </xhtml:span>
</xsl:template>
<xsl:template match="ld:GRef">
- <span class="gref">
+ <xhtml:span class="gref" title="{@position}<{@uri}>">
<xsl:call-template name="uri"/>
- </span>
+ </xhtml:span>
</xsl:template>
<xsl:template match="ld:Cast">
- <span class="cast">
+ <xhtml:span class="cast">
<xsl:call-template name="oa"/>
- <xsl:apply-templates/>
+ <xsl:apply-templates select="*"/>
<xsl:call-template name="ca"/>
- </span>
+ </xhtml:span>
<xsl:call-template name="separator"/>
</xsl:template>
<xsl:template match="ld:Appl">
- <span class="appl">
+ <xhtml:span class="appl">
<xsl:call-template name="op"/>
- <xsl:call-template name="mk_terms"/>
+ <xsl:apply-templates select="*"/>
+<!-- <xsl:call-template name="mk_terms"/> -->
<xsl:call-template name="cp"/>
- </span>
+ </xhtml:span>
+ <xsl:call-template name="separator"/>
+</xsl:template>
+
+<xsl:template match="ld:Proj">
+ <xhtml:span class="proj">
+ <xsl:call-template name="oc"/>
+ <xsl:apply-templates select="*"/>
+ <xsl:call-template name="cc"/>
+ </xhtml:span>
<xsl:call-template name="separator"/>
</xsl:template>
<xsl:template match="ld:Abst">
- <span class="local">
- <xsl:call-template name="lambda"/>
- <xsl:call-template name="mk_binder">
- <xsl:with-param name="sep-seq">
- <xsl:call-template name="cn"/>
- </xsl:with-param>
- </xsl:call-template>
- </span>
+ <xhtml:span class="local" title="{@position}">
+ <xsl:call-template name="abst"/>
+ <xsl:call-template name="ob"/>
+ <xsl:call-template name="name"/>
+ <xsl:call-template name="cn"/>
+ <xsl:apply-templates select="*"/>
+ <xsl:call-template name="cb"/>
+ </xhtml:span>
<xsl:call-template name="separator"/>
</xsl:template>
<xsl:template match="ld:Abbr">
- <span class="local">
- <xsl:call-template name="delta"/>
- <xsl:call-template name="mk_binder">
- <xsl:with-param name="sep-seq">
- <xsl:call-template name="eq"/>
- </xsl:with-param>
- </xsl:call-template>
- </span>
+ <xhtml:span class="local">
+ <xsl:call-template name="abbr"/>
+ <xsl:call-template name="ob"/>
+ <xsl:call-template name="name"/>
+ <xsl:call-template name="eq"/>
+ <xsl:apply-templates select="*"/>
+ <xsl:call-template name="cb"/>
+ </xhtml:span>
<xsl:call-template name="separator"/>
</xsl:template>
<xsl:template match="ld:Void">
- <span class="local">
- <xsl:call-template name="chi"/>
+ <xhtml:span class="local">
+ <xsl:call-template name="void"/>
<xsl:call-template name="ob"/>
- <xsl:call-template name="mk_names"/>
+ <xsl:call-template name="name"/>
<xsl:call-template name="cb"/>
- </span>
+ </xhtml:span>
<xsl:call-template name="separator"/>
</xsl:template>
projects / helm.git / commitdiff