<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 29 Dec 2015 22:50:57 +0100</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 14:56:06 +0100</div>
</body>
</html>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 12:08:04 +0100</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 14:54:53 +0100</div>
</body>
</html>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 29 Dec 2015 22:50:57 +0100</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 14:56:06 +0100</div>
</body>
</html>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 12:08:04 +0100</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 14:56:06 +0100</div>
</body>
</html>
<li>
C. Dunchev, F. Guidi, C. Sacerdoti Coen, E. Tassi:
<span class="emph alpha">ELPI: fast, Embeddable, λProlog Interpreter</span>
- (2015). In proc. of LPAR 20. LNCS 9450, pp. 460-468.
+ (2015). In proc. of LPAR 20. Lecture Notes in Computer Science, 9450, pp. 460-468. Springer.
</li>
</ul>
<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.
+ (2012). In Journal of Automated Reasoning, 49(3), pp. 427-451. Springer.
</li>
</ul>
<ul xmlns:ld="http://lambdadelta.info/" id="C5">
<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.
+ (2009). In Annals of Pure and Applied Logic, 160(3), pp. 319-354. Elsevier.
</li>
</ul>
<ul xmlns:ld="http://lambdadelta.info/" id="C1">
<div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="disclaimer">Disclaimer <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b9.png" />
</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
- The systens of the λδ family <span xmlns="http://lambdadelta.info/" class="emph">are not</span> related intentionally to any other system
+ The systens of the λδ family <span class="emph alpha">are not</span> related intentionally to any other system
having (variations of) the symbols λ and δ in its name or syntax.
Examples include (but are not limited to):
</div>
<ul xmlns:ld="http://lambdadelta.info/" id="D1">
<li>
- <span xmlns="http://lambdadelta.info/" class="emph">λ-δ</span> of
+ <span class="emph alpha">λ-δ</span> of
A. Church:
- <span xmlns="http://lambdadelta.info/" class="emph">The calculi of lambda-conversion</span>
+ <span class="emph alpha">The calculi of lambda-conversion</span>
(1941).
Annals of Mathematics Studies 6.
Princeton University Press.
</ul>
<ul xmlns:ld="http://lambdadelta.info/" id="D2">
<li>
- <span xmlns="http://lambdadelta.info/" class="emph">∆Λ</span> of
+ <span class="emph alpha">∆Λ</span> of
N.G. de Bruijn:
- <span xmlns="http://lambdadelta.info/" class="emph">Generalizing Automath by means of a lambda-typed lambda calculus</span>
+ <span class="emph alpha">Generalizing Automath by means of a lambda-typed lambda calculus</span>
(1987).
In Lecture Notes in Pure and Applied Mathematics 106, pp. 71-92.
Marcel Dekker.
</ul>
<ul xmlns:ld="http://lambdadelta.info/" id="D3">
<li>
- <span xmlns="http://lambdadelta.info/" class="emph">λ<sub>∆</sub>
+ <span class="emph alpha">λ<sub xmlns="http://lambdadelta.info/">∆</sub>
</span> of
N.J. Rehof, M.H. Sørensen:
- <span xmlns="http://lambdadelta.info/" class="emph">The λ<sub>∆</sub>-calculus</span>
+ <span class="emph alpha">The λ<sub xmlns="http://lambdadelta.info/">∆</sub>-calculus</span>
(1994).
In Lecture Notes in Computer Science, 789, pp. 516–542.
Springer.
</ul>
<ul xmlns:ld="http://lambdadelta.info/" id="D4">
<li>
- <span xmlns="http://lambdadelta.info/" class="emph alpha">λ∆</span> of
+ <span class="emph alpha">λ∆</span> of
S. Ronchi Della Rocca, L. Paolini:
- <span xmlns="http://lambdadelta.info/" class="emph">The Parametric Lambda Calculus</span>
+ <span class="emph alpha">The Parametric Lambda Calculus</span>
(2004).
Texts in Theoretical Computer Science, An EATCS Series.
Springer.
</ul>
<ul xmlns:ld="http://lambdadelta.info/" id="D5">
<li>
- <span xmlns="http://lambdadelta.info/" class="emph">λD</span> of
+ <span class="emph alpha">λD</span> of
R. Nederpelt, H. Geuvers:
- <span xmlns="http://lambdadelta.info/" class="emph">Type Theory and Formal Proof</span>
+ <span class="emph alpha">Type Theory and Formal Proof</span>
(2014).
Cambridge University Press.
</li>
</ul>
<ul xmlns:ld="http://lambdadelta.info/" id="D6">
<li>
- <span xmlns="http://lambdadelta.info/" class="emph">Cλξ</span> of
+ <span class="emph alpha">Cλξ</span> of
N.G. de Bruijn:
- <span xmlns="http://lambdadelta.info/" class="emph">A namefree lambda calculus with facilities for internal definition of expressions and segments</span>
+ <span class="emph alpha">A namefree lambda calculus with facilities for internal definition of expressions and segments</span>
(1978).
TH-report 78-WSK-03.
Eindhoven University of Technology, Eindhoven.
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 12:08:04 +0100</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 14:56:06 +0100</div>
</body>
</html>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 12:08:03 +0100</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 14:54:53 +0100</div>
</body>
</html>
<div xmlns:ld="http://lambdadelta.info/" class="text">
Informational pages on the specifications are provided.
</div>
- <ul xmlns:ld="http://lambdadelta.info/" id="">
+ <ul xmlns:ld="http://lambdadelta.info/" id="notice1">
<li>
<span class="emph alpha">Notice on displayed numerical acounts:</span>
nodes are counted according to the "intrinsic complexity measure"
Journal of Automated Reasoning 44(1-2), Springer (February 2010), pp. 53-78].
</li>
</ul>
- <ul xmlns:ld="http://lambdadelta.info/" id="">
+ <ul xmlns:ld="http://lambdadelta.info/" id="notice2">
<li>
<span class="emph alpha">Notice on displayed logical structures:</span>
from the logical standpoint, the source scripts are grouped in "planes"
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 12:08:04 +0100</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 14:54:53 +0100</div>
</body>
</html>
</body>
<body>
This is the family logo: <rlink to="images/crux_177.png">crux_177.png</rlink>
- (revised <notice class="alpha" notice="2012-09"/>).
+ (revised <notice class="alpha" text="2012-09"/>).
</body>
<body>
- <notice class="alpha" notice="Notice for the user of Internet Explorer."/>
+ <notice class="alpha" text="Notice for the user of Internet Explorer."/>
To view this site correctly, please select a font
with <link to="http://www.unicode.org/">Unicode</link> support.
For example "Lucida Sans Unicode" (it should be already installed on your system).
<topitem name="C7">
C. Dunchev, F. Guidi, C. Sacerdoti Coen, E. Tassi:
- <notice class="alpha" notice="ELPI: fast, Embeddable, λProlog Interpreter"/>
- (2015). In proc. of LPAR 20. LNCS 9450, pp. 460-468.
+ <notice class="alpha">ELPI: fast, Embeddable, λProlog Interpreter</notice>
+ (2015). In proc. of LPAR 20. Lecture Notes in Computer Science, 9450, pp. 460-468. Springer.
</topitem>
<topitem name="C6">
A. Asperti, W. Ricciotti, C. Sacerdoti Coen, E. Tassi:
- <notice class="alpha" notice="Formal metatheory of programming languages in the Matita interactive theorem prover"/>
- (2012). In JAR 49(3), pp. 427-451.
+ <notice class="alpha">Formal metatheory of programming languages in the Matita interactive theorem prover</notice>
+ (2012). In Journal of Automated Reasoning, 49(3), pp. 427-451. Springer.
</topitem>
<topitem name="C5">
M.E. Maietti:
- <notice class="alpha" notice="Consistency of the minimalist foundation with Church thesis and Bar Induction"/>
+ <notice class="alpha">Consistency of the minimalist foundation with Church thesis and Bar Induction</notice>
(2012). Submitted article.
</topitem>
<topitem name="C4">
W. Ricciotti:
- <notice class="alpha" notice="Theoretical and implementation aspects in the mechanization of the metatheory of programming languages"/>
+ <notice class="alpha">Theoretical and implementation aspects in the mechanization of the metatheory of programming languages</notice>
(July 2011). Ph.D. Thesis in Computer Science, Technical Report UBLCS-2011-09, University of Bologna.
</topitem>
<topitem name="C3">
C.E. Brown:
- <notice class="alpha" notice="Faithful Reproductions of the Automath Landau Formalization"/>
+ <notice class="alpha">Faithful Reproductions of the Automath Landau Formalization</notice>
(2011). Technical report.
</topitem>
<topitem name="C2">
M.E. Maietti:
- <notice class="alpha" notice="A minimalist two-level foundation for constructive mathematics"/>
- (2009). In APAL 160(3), pp. 319-354.
+ <notice class="alpha">A minimalist two-level foundation for constructive mathematics</notice>
+ (2009). In Annals of Pure and Applied Logic, 160(3), pp. 319-354. Elsevier.
</topitem>
<topitem name="C1">
V. Rahili:
- <notice class="alpha" notice="First Year Report: Realisability methods of proof and semantics with application to expansion"/>
+ <notice class="alpha">First Year Report: Realisability methods of proof and semantics with application to expansion</notice>
(July 2007). Technical report.
</topitem>
<section9 name="disclaimer">Disclaimer</section9>
<body>
- The systens of the λδ family <span class="emph">are not</span> related intentionally to any other system
+ The systens of the λδ family <notice class="alpha" text="are not"/> related intentionally to any other system
having (variations of) the symbols λ and δ in its name or syntax.
Examples include (but are not limited to):
</body>
<topitem name="D1">
- <span class="emph">λ-δ</span> of
+ <notice class="alpha">λ-δ</notice> of
A. Church:
- <span class="emph">The calculi of lambda-conversion</span>
+ <notice class="alpha">The calculi of lambda-conversion</notice>
(1941).
Annals of Mathematics Studies 6.
Princeton University Press.
</topitem>
<topitem name="D2">
- <span class="emph">∆Λ</span> of
+ <notice class="alpha">∆Λ</notice> of
N.G. de Bruijn:
- <span class="emph">Generalizing Automath by means of a lambda-typed lambda calculus</span>
+ <notice class="alpha">Generalizing Automath by means of a lambda-typed lambda calculus</notice>
(1987).
In Lecture Notes in Pure and Applied Mathematics 106, pp. 71-92.
Marcel Dekker.
</topitem>
<topitem name="D3">
- <span class="emph">λ<sub>∆</sub></span> of
+ <notice class="alpha">λ<sub>∆</sub></notice> of
N.J. Rehof, M.H. Sørensen:
- <span class="emph">The λ<sub>∆</sub>-calculus</span>
+ <notice class="alpha">The λ<sub>∆</sub>-calculus</notice>
(1994).
In Lecture Notes in Computer Science, 789, pp. 516–542.
Springer.
</topitem>
<topitem name="D4">
- <span class="emph alpha">λ∆</span> of
+ <notice class="alpha">λ∆</notice> of
S. Ronchi Della Rocca, L. Paolini:
- <span class="emph">The Parametric Lambda Calculus</span>
+ <notice class="alpha">The Parametric Lambda Calculus</notice>
(2004).
Texts in Theoretical Computer Science, An EATCS Series.
Springer.
</topitem>
<topitem name="D5">
- <span class="emph">λD</span> of
+ <notice class="alpha">λD</notice> of
R. Nederpelt, H. Geuvers:
- <span class="emph">Type Theory and Formal Proof</span>
+ <notice class="alpha">Type Theory and Formal Proof</notice>
(2014).
Cambridge University Press.
</topitem>
<topitem name="D6">
- <span class="emph">Cλξ</span> of
+ <notice class="alpha">Cλξ</notice> of
N.G. de Bruijn:
- <span class="emph">A namefree lambda calculus with facilities for internal definition of expressions and segments</span>
+ <notice class="alpha">A namefree lambda calculus with facilities for internal definition of expressions and segments</notice>
(1978).
TH-report 78-WSK-03.
Eindhoven University of Technology, Eindhoven.
</body>
<body>
The life cycle of a specification consists of four periods.
- <notice class="alpha" notice="Alpha:"/>
+ <notice class="alpha" text="Alpha:"/>
the definitions are designed and the major propositions are proved,
then the calculus is announced with a presentation.
- <notice class="beta" notice="Beta:"/>
+ <notice class="beta" text="Beta:"/>
major changes and additions may occur before the calculus is released on paper.
- <notice class="gamma" notice="Gamma:"/>
+ <notice class="gamma" text="Gamma:"/>
subsequent improvements occur until the specification is completed or superseded,
while major changes and additions are announced and reported on paper.
- <notice class="delta" notice="Delta:"/>
+ <notice class="delta" text="Delta:"/>
after its conclusion, the specification is modified just for maintenance.
</body>
<table name="versions"/>
<body>
Informational pages on the specifications are provided.
</body>
- <topitem>
- <notice class="alpha" notice="Notice on displayed numerical acounts:"/>
+ <topitem name="notice1">
+ <notice class="alpha" text="Notice on displayed numerical acounts:"/>
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].
</topitem>
- <topitem>
- <notice class="alpha" notice="Notice on displayed logical structures:"/>
+ <topitem name="notice2">
+ <notice class="alpha" text="Notice on displayed logical structures:"/>
from the logical standpoint, the source scripts are grouped in "planes"
and these are grouped in "components";
the notation for the relations or functions
<topitem name="source2">
<body>
<rlink to="download/lambdadelta_2A1.tar.gz">lambdadelta_2A1 for Matita 0.99.2</rlink>
- (revised <notice class="gamma" notice="2014-10"/>).
+ (revised <notice class="gamma" text="2014-10"/>).
Source scripts.
<rlink to="documentation.html#ldR2c">Documentation (R2c)</rlink>.
</body>
The scripts are grouped in directories, first by part, then by component.
</body>
<body>
- <notice class="alpha" notice="Notice:"/>
+ <notice class="alpha" text="Notice:"/>
the scripts are checked by the latest version of Matita from
<link to="http://matita.cs.unibo.it/download.shtml">HELM Subversion repository</link>
at path <trunk/matita/>.
<topitem name="source1">
<body>
<rlink to="download/lambdadelta_1.tar.gz">lambdadelta_1 for Coq 7.3.1</rlink>
- (revised <notice class="delta" notice="2015-09"/>).
+ (revised <notice class="delta" text="2015-09"/>).
Source scripts.
<rlink to="documentation.html#ldJ1a">Documentation (J1a)</rlink>.
<list><item>
- <notice class="delta" notice="2015 January 15."/>
+ <notice class="delta" text="2015 January 15."/>
17 new lemmas and former lemma "eq_nat_dec" renamed as "nat_dec_neg".
</item></list>
</body>
<topitem name="static1">
<rlink to="static/matita/lambdadelta/">lambdadelta_1 for Matita 0.5</rlink>
- (revised <notice class="delta" notice="2011-09"/>).
+ (revised <notice class="delta" text="2011-09"/>).
Static HTML pages generated by the <link to="http://helm.cs.unibo.it/">HELM</link> rendering engine.
<list><item>
<rlink to="static/matita/lambdadelta/basic_1/pr3/pr3/pr3_confluence.con.html">
<topitem name="dynamic1">
<link to="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</link>
- (revised <notice class="delta" notice="2011-09"/>).
+ (revised <notice class="delta" text="2011-09"/>).
<link to="http://helm.cs.unibo.it/">HELM</link> directory.
- <notice class="alpha" notice="Notice: the HELM rendering engine is offline."/>
+ <notice class="alpha" text="Notice: the HELM rendering engine is offline."/>
</topitem>
<body>
</xsl:template>
<xsl:template match="ld:notice">
- <span class="emph {@class}"><xsl:value-of select="@notice"/></span>
+ <span class="emph {@class}">
+ <xsl:choose>
+ <xsl:when test="@notice"><xsl:value-of select="@notice"/></xsl:when>
+ <xsl:when test="@text"><xsl:value-of select="@text"/></xsl:when>
+ <xsl:otherwise><xsl:apply-templates/></xsl:otherwise>
+ </xsl:choose>
+ </span>
</xsl:template>
<xsl:template match="ld:version3-icon">
projects / helm.git / commitdiff