]> matita.cs.unibo.it Git - helm.git/blob - helm/www/lambdadelta/web/home/news.ldw.xml
- update in basic_2
[helm.git] / helm / www / lambdadelta / web / home / news.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       head = "The Formal System λδ (\lambda\delta)"
7 >
8    <sitemap name="sitemap"/>
9
10 <!-- ===================================================================== -->
11
12    <section3 name="milestones">Milestones</section3>
13
14    <news date="July 2014.">
15       A new version of this site is online.
16    </news>
17
18    <news date="June 2014.">
19       <rlink to="documentation.html#ldP8">First communication on λδ version 2.</rlink>
20    </news>
21
22    <news date="December 2012.">
23       The character "_" is removed from the denomination "lambda_delta":
24       <list><item>
25          The denomination "\lambda\delta" is used in λδ-related texts.
26       </item><item>
27          The denomination "lambdadelta" is used in λδ-related identifiers.
28       </item><item>
29          Permanent λδ URL acquired:
30          <rlink to="">http://lambdadelta.info/</rlink>
31          (pointing at this site).
32       </item></list>
33    </news>
34
35    <news date="September 2011.">
36       The denomination "lambda-delta" changes to "lambda_delta":
37       <list><item>
38          The character "-" is reserved in λδ textual syntax
39          (recognized by "Helena 0.8.1").            
40       </item><item>
41          Eventually, the occurrences of the character "-"
42          will be replaced by "_" in all λδ-related identifiers.
43       </item><item>
44          In particular, this refactoring involves file names and path names.
45       </item></list>
46    </news>
47
48    <news date="April 2011.">
49       The specification of <rlink to="version_2.html">λδ version 2</rlink>
50       and related topics is restarted in
51       <link to="http://matita.cs.unibo.it/">Matita 0.5</link>.
52    </news>
53
54    <news date="December 2010.">
55       Transient λδ URL acquired: http://lambda-delta.info/ (expires on December 2012). 
56    </news>
57
58    <news date="November 2010.">
59       "Helena 0.8.1" is released. 
60    </news>
61
62    <news date="September 2009.">
63       "Helena 0.8.0" is released and the
64       <rlink to="implementation.html#lddl">λδ Digital Library</rlink>
65       is started.
66    </news>
67
68    <news date="June 2009.">
69       "Helena", a <rlink to="implementation.html#helena">validator for λδ version 2</rlink>,
70       is available as a part of the <link to="http://helm.cs.unibo.it/">HELM</link> software. 
71    </news>
72
73    <news date="September 2008.">
74       This site is online.
75    </news>
76
77    <news date="July 2008.">
78       <rlink to="documentation.html#ldJ1">First journal paper on λδ</rlink>
79       accepted for publication.
80    </news>
81
82    <news date="July 2008.">
83       First <link to="http://helm.cs.unibo.it/procedural/">procedural reconstruction</link>
84       for <link to="http://matita.cs.unibo.it/">Matita 0.5</link>
85       of the λδ version 1 for Coq 7.3.1.
86    </news>
87
88    <news date="June 2008.">
89       The <rlink to="version_1.html#static">
90          HTML pages of the specification of λδ version 1 for Matita 0.5</rlink>
91       are online.
92    </news>
93
94    <news date="May 2008.">
95       The specification of λδ version 1 is dismissed.
96    </news>
97
98    <news date="March 2008.">
99       The specification of λδ version 2 is started with Coq 7.3.1 (false start).
100    </news>
101
102    <news date="September 2007.">
103       The <rlink to="version_1.html#dynamic">
104          specification of λδ version 1 for Matita 0.4</rlink>
105       is online.
106    </news>
107
108    <news date="November 2006.">
109       <rlink to="documentation.html#ldR2">λδ version 1</rlink>
110       is released.
111    </news>
112
113    <news date="December 2005.">
114       <rlink to="documentation.html#ldP1">First communication on λδ version 1</rlink>.
115    </news>
116
117    <news date="May 2004.">
118       The specification of <rlink to="version_1.html">λδ version 1</rlink>
119       is started with Coq 7.3.1.
120    </news>
121
122 <!-- ===================================================================== -->
123
124    <section3 name="citations">Citations</section3>
125    <body>
126       Here is a list of publications citing λδ (not including our own).
127    </body>
128
129    <topitem name="C6">
130       A. Asperti, W. Ricciotti, C. Sacerdoti Coen, E. Tassi:
131       <date date="Formal metatheory of programming languages in the Matita interactive theorem prover"/>
132       (2012). In JAR 49(3), pp. 427-451.
133    </topitem>
134
135    <topitem name="C5">
136       M.E. Maietti:
137       <date date="Consistency of the minimalist foundation with Church thesis and Bar Induction"/>
138       (2012). Submitted article.
139    </topitem>
140
141    <topitem name="C4">
142       W. Ricciotti:
143       <date date="Theoretical and implementation aspects in the mechanization of the metatheory of programming languages"/>
144       (July 2011). Ph.D. Thesis in Computer Science, Technical Report UBLCS-2011-09, University of Bologna.
145    </topitem>
146
147    <topitem name="C3">
148       C.E. Brown:
149       <date date="Faithful Reproductions of the Automath Landau Formalization"/>
150       (2011). Typescript note.
151    </topitem>
152
153    <topitem name="C2">
154       M.E. Maietti:
155       <date date="A minimalist two-level foundation for constructive mathematics"/>
156       (2009). In APAL 160(3), pp. 319-354.
157    </topitem>
158
159    <topitem name="C1">
160       V. Rahili: 
161       <date date="First Year Report: Realisability methods of proof and semantics with application to expansion"/>
162       (July 2007). Typescript note.
163    </topitem>
164
165 <!-- ===================================================================== -->
166
167    <section3 name="visibility">Visibility</section3>
168
169    <news date="June 2014.">
170       The <link to="http://www.google.com/">Google</link>
171       search for "formal system lambda delta" gives
172       5 resources about λδ in the first 6 results.
173    </news>
174
175    <news date="June 2014.">
176       The <link to="http://www.yahoo.com/">Yahoo</link>
177       search for "formal system lambda delta" gives
178       4 resources about λδ in the first 5 results.
179    </news>
180
181    <footer/>
182 </page>