]> matita.cs.unibo.it Git - helm.git/blob - helm/www/lambdadelta/web/home/home.ldw.xml
update in basic_2
[helm.git] / helm / www / lambdadelta / web / home / home.ldw.xml
1 <?xml version="1.0" encoding="UTF-8"?>
2
3 <page xmlns="http://lambdadelta.info/"
4       description = "\lambda\delta home page"
5       title = "\lambda\delta home page"
6       logo = "crux"
7       head = "The Formal Systems of the λδ (\lambda\delta) Family"
8 >
9    <sitemap name="sitemap"/>
10
11    <section9 name="foreword">Foreword</section9>
12    <body>
13       The formal systems of the λδ (\lambda\delta) family are typed λ-calculi aiming to support
14       the foundational frameworks for Mathematics that require an underlying specification language
15       (for example the <link to="http://www.math.unipd.it/~maietti/">Minimalist Foundation</link>
16        and its predecessors).
17    </body>
18    <body>
19       The λδ family is developed within the
20       <link to="http://helm.cs.unibo.it/">Hypertextual Electronic Library of Mathematics</link>
21       as a set of machine-checked digital specifications.
22    </body>
23    <body>
24       This is the family logo: <rlink to="images/crux_177.png">crux_177.png</rlink>
25       (revised <notice class="alpha" text="2012-09"/>).
26    </body>
27    <body>
28       <notice class="alpha" text="Notice for the user of Internet Explorer."/>
29       To view this site correctly, please select a font
30       with <link to="http://www.unicode.org/">Unicode</link> support.
31       For example "Lucida Sans Unicode" (it should be already installed on your system).
32       To change the current font follow:
33       "Tools" menu → "Internet Options" entry → "General" tab → "Fonts" button.
34    </body>
35
36 <!-- ===================================================================== -->
37
38    <section9 name="citations">Citations</section9>
39    <body>
40       This is a list of publications citing λδ documentation.
41    </body>
42
43    <topitem name="C9">
44       Matthias Weber:
45       <notice class="alpha">An extended type system with lambda-typed lambda-expressions (extended version)</notice>
46       (2017). Technical report. Faculty of Computer Science, Technical University of Berlin.
47    </topitem>
48
49    <topitem name="C8">
50       M.E. Maietti, S. Maschio:
51       <notice class="alpha">An extensional Kleene realizability semantics for the Minimalist Foundation</notice>
52       (2015). In Leibniz International Proceedings in Informatics, 39, pp 162-186. Schloss Dagstuhl, Leibniz-Zentrum für Informatik.
53    </topitem>
54
55    <topitem name="C7">
56       C. Dunchev, F. Guidi, C. Sacerdoti Coen, E. Tassi:
57       <notice class="alpha">ELPI: Fast, Embeddable, λProlog Interpreter</notice>
58       (2015). In proc. of LPAR 20. Lecture Notes in Computer Science, 9450, pp. 460-468. Springer.
59    </topitem>
60
61    <topitem name="C6">
62       A. Asperti, W. Ricciotti, C. Sacerdoti Coen, E. Tassi:
63       <notice class="alpha">Formal metatheory of programming languages in the Matita interactive theorem prover</notice>
64       (2012). In Journal of Automated Reasoning, 49(3), pp. 427-451. Springer.
65    </topitem>
66
67    <topitem name="C5">
68       M.E. Maietti:
69       <notice class="alpha">Consistency of the minimalist foundation with Church thesis and Bar Induction</notice>
70       (2012). Submitted article.
71    </topitem>
72
73    <topitem name="C4">
74       W. Ricciotti:
75       <notice class="alpha">Theoretical and implementation aspects in the mechanization of the metatheory of programming languages</notice>
76       (July 2011). Ph.D. Thesis in Computer Science, Technical Report UBLCS-2011-09, University of Bologna.
77    </topitem>
78
79    <topitem name="C3">
80       C.E. Brown:
81       <notice class="alpha">Faithful Reproductions of the Automath Landau Formalization</notice>
82       (2011). Technical report.
83    </topitem>
84
85    <topitem name="C2">
86       M.E. Maietti:
87       <notice class="alpha">A minimalist two-level foundation for constructive mathematics</notice>
88       (2009). In Annals of Pure and Applied Logic, 160(3), pp. 319-354. Elsevier. 
89    </topitem>
90
91    <topitem name="C1">
92       V. Rahili: 
93       <notice class="alpha">First Year Report: Realisability methods of proof and semantics with application to expansion</notice>
94       (July 2007). Technical report.
95    </topitem>
96
97 <!-- ===================================================================== -->
98
99    <section9 name="disclaimer">Disclaimer</section9>
100    <body>
101       The systems of the λδ family <notice class="alpha" text="are not"/> related intentionally to
102       any other system having (variations of) the symbols λ and δ in its name or syntax.
103       Examples include (but are not limited to):
104    </body>
105
106    <topitem name="D1">
107       <notice class="alpha">λ-δ</notice> of
108       A. Church:
109       <notice class="alpha">The calculi of lambda-conversion</notice>
110       (1941).
111       Annals of Mathematics Studies 6.
112       Princeton University Press.
113    </topitem>
114
115    <topitem name="D2">
116       <notice class="alpha">∆Λ</notice> of
117       N.G. de Bruijn:
118       <notice class="alpha">Generalizing Automath by means of a lambda-typed lambda calculus</notice>
119       (1987).
120       In Lecture Notes in Pure and Applied Mathematics 106, pp. 71-92.
121       Marcel Dekker.
122    </topitem>
123
124    <topitem name="D3">
125       <notice class="alpha">λ<sub>∆</sub></notice> of
126       N.J. Rehof, M.H. Sørensen:
127       <notice class="alpha">The λ<sub>∆</sub>-calculus</notice>
128       (1994).
129       In Lecture Notes in Computer Science, 789, pp. 516–542.
130       Springer.
131    </topitem>
132
133    <topitem name="D4">
134       <notice class="alpha">λ∆</notice> of
135       S. Ronchi Della Rocca, L. Paolini:
136       <notice class="alpha">The Parametric Lambda Calculus</notice>
137       (2004).
138       Texts in Theoretical Computer Science, An EATCS Series.
139       Springer.
140    </topitem>
141
142    <topitem name="D5">
143       <notice class="alpha">λD</notice> of
144       R. Nederpelt, H. Geuvers:
145       <notice class="alpha">Type Theory and Formal Proof</notice>
146       (2014).
147       Cambridge University Press.
148    </topitem>
149
150    <topitem name="D6">
151       <notice class="alpha">Cλξ</notice> of
152       N.G. de Bruijn:
153       <notice class="alpha">A namefree lambda calculus with facilities for internal definition of expressions and segments</notice>
154       (1978).
155       TH-report 78-WSK-03.
156       Eindhoven University of Technology, Eindhoven.
157    </topitem>
158
159    <body>
160       <img logo="smile"/>
161       Moreover, the systems of the λδ family <notice class="alpha" text="are not"/> related intentionally to
162       <link to="http://umineko.wikia.com/wiki/Lambdadelta">Lady Lambdadelta</link>,
163       the Witch of Certainty of the sound novel
164       <link to="https://it.wikipedia.org/wiki/Umineko_no_naku_koro_ni">Umineko no Naku Koro ni</link>.
165    </body>
166
167    <footer/>
168 </page>