106 <HR> |
106 <HR> |
107 |
107 |
108 |
108 |
109 <p> |
109 <p> |
110 The 6th conference on Interactive Theorem Proving was held in |
110 The 6th conference on Interactive Theorem Proving was held in |
111 Nanjing, China. |
111 Nanjing, China. The proceedings were published as usual in the |
112 <A HREF="http://en.wikipedia.org/wiki/Nanjing">Nanjing</A> is situated |
|
113 in the heart of China — close to Shanghai and roughly |
|
114 equidistant between Beijing and Hong Kong. It is a former capital |
|
115 during the Ming Dynasty with a rich <A |
|
116 HREF="http://www.cityofnanjing.com">cultural heritage</A>. |
|
117 The proceedings will be published as usual in the |
|
118 <A HREF="http://link.springer.com/book/10.1007/978-3-319-22102-1">LNCS</A> |
112 <A HREF="http://link.springer.com/book/10.1007/978-3-319-22102-1">LNCS</A> |
119 Series. There was an |
113 Series. There was an |
120 <A HREF="http://www21.in.tum.de/~nipkow/isa-tut-itp15.html">Isabelle tutorial</A> before the |
114 <A HREF="http://www21.in.tum.de/~nipkow/isa-tut-itp15.html">Isabelle tutorial</A> before the |
121 conference (21 - 23 August), and |
115 conference (21 - 23 August), and |
122 a <A HREF="coq.pdf">Coq tutorial</A> after the conference |
116 a <A HREF="coq.pdf">Coq tutorial</A> after the conference |
143 <img src="itp-photo-small.jpg" width="400" height="200"></a> |
137 <img src="itp-photo-small.jpg" width="400" height="200"></a> |
144 </center> |
138 </center> |
145 |
139 |
146 <H4><A NAME="programme">Programme</H4> |
140 <H4><A NAME="programme">Programme</H4> |
147 |
141 |
148 As is the tradition, the conference consists of 4 days |
142 As is the tradition, the conference consisted of 4 days |
149 of research presentations and invited talks. Like in previous |
143 of research presentations and invited talks. Like in previous |
150 conferences, we will have ample time between the formal sessions for |
144 conferences, there was ample time between the formal sessions for |
151 attendees to mingle and converse. Half a day will be dedicated to an |
145 attendees to mingle and converse. Half a day was dedicated to an |
152 excursion to <A HREF="http://en.wikipedia.org/wiki/Yangzhou">Yangzhou</A> |
146 excursion to <A HREF="http://en.wikipedia.org/wiki/Yangzhou">Yangzhou</A> |
153 and the <A HREF="http://en.wikipedia.org/wiki/Yangzhou#Slender_West_Lake">Slender West Lake</A>. |
147 and the <A HREF="http://en.wikipedia.org/wiki/Yangzhou#Slender_West_Lake">Slender West Lake</A>. |
154 The preliminary programme of talks can be found |
148 The programme of talks can be found |
155 <A HREF="prog1.pdf">here</A>. |
149 <A HREF="prog1.pdf">here</A>. |
156 |
150 |
157 |
151 |
158 <H4><A NAME="travel">Travel to Nanjing</H4> |
152 <H4><A NAME="travel">Travel to Nanjing</H4> |
159 |
153 |
196 transfer; we <span style="text-decoration: underline;"><B>cannot</B></span> |
190 transfer; we <span style="text-decoration: underline;"><B>cannot</B></span> |
197 accept credit cards etc for the conference fee. The hotel and many other things can be paid |
191 accept credit cards etc for the conference fee. The hotel and many other things can be paid |
198 by credit card, but not the conference fee. See the <A HREF="booklet5.pdf">booklet</A> for |
192 by credit card, but not the conference fee. See the <A HREF="booklet5.pdf">booklet</A> for |
199 details about the bank transfer. |
193 details about the bank transfer. |
200 |
194 |
201 <H4>Venue and Accommodation</H4> |
|
202 |
|
203 The conference will take place at the |
|
204 <A HREF="http://english.ctrip.com/hotels/nanjing-hotel-detail-66456/nanjing-hanyuan-mansion-center-of-academic-exchange/">Hanyuan |
|
205 Hotel</A>, which is relatively inexpensive |
|
206 (ca. 390元/£34/$52/€47 per night including breakfast) |
|
207 and in easy reach from the city centre |
|
208 <!-- (see <A HREF="https://maps.google.com/maps?q=Hanyuan+Mansion,+20+Tongwei+Road,+Xuanwu,+Nanjing,+Jiangsu,+China,+210095&hl=en&ll=32.029617,118.838768&spn=0.204033,0.292854&sll=32.010405,118.824692&sspn=0.204076,0.292854&t=m&z=12">here</A> |
|
209 at Google Maps). --> |
|
210 The conference hotel has the usual amenities (Wifi, conference rooms, etc) |
|
211 and includes a restaurant. |
|
212 We have reserved some rooms in the hotel for participants. See the |
|
213 <A HREF="booklet5.pdf">booklet</A> for information about the hotel booking. |
|
214 |
|
215 |
|
216 <p> |
|
217 <center> |
|
218 <table style="width: 75%"> |
|
219 <tr> |
|
220 <td> |
|
221 <img src="pics/hotel1.jpg" alt="hotel" width="98%" height="21%" border=0> |
|
222 </td> |
|
223 <td> |
|
224 <img src="pics/hotel2.jpg" alt="hotel" width="98%" height="21%" border=0> |
|
225 </td> |
|
226 <td> |
|
227 <img src="pics/hotel4.jpg" alt="hotel" width="98%" height="21%" border=0> |
|
228 </td> |
|
229 </tr> |
|
230 <tr> |
|
231 <td colspan="3"><center><small>Hanyuan Hotel</small></center></td> |
|
232 </tr> |
|
233 </table> |
|
234 </center> |
|
235 |
|
236 <p> |
|
237 There are also many additional |
|
238 <A HREF="http://wikitravel.org/en/Nanjing#Sleep">hotels</A> in all price categories nearby. |
|
239 Also there are innumerable <A |
|
240 HREF="http://www.chinatour.com/nanjing/nanjing-food.htm">restaurants</A> in the area. |
|
241 |
|
242 |
195 |
243 <H4>Local Information</H4> |
196 <H4>Local Information</H4> |
244 |
|
245 |
|
246 |
197 |
247 <p> |
198 <p> |
248 Being in China, Nanjing offers the usual conveniences of good and |
199 Being in China, Nanjing offers the usual conveniences of good and |
249 affordable food. It has several excellent |
200 affordable food. It has several excellent |
250 <A HREF="http://en.wikipedia.org/wiki/Nanjing#Museums">museums</A> |
201 <A HREF="http://en.wikipedia.org/wiki/Nanjing#Museums">museums</A> |
263 Nanjing's Confucius Temple. |
214 Nanjing's Confucius Temple. |
264 |
215 |
265 |
216 |
266 <H4>Excursion</H4> |
217 <H4>Excursion</H4> |
267 |
218 |
268 The excursion will be to |
219 The excursion went to |
269 <A HREF="http://en.wikipedia.org/wiki/Yangzhou">Yangzhou</A> (1h away |
220 <A HREF="http://en.wikipedia.org/wiki/Yangzhou">Yangzhou</A> (1h away |
270 from Nanjing by bus). The tour will include a walk |
221 from Nanjing by bus). We walked |
271 around the Slender West Lake with its pavilions, the white Lotus |
222 around the Slender West Lake with its pavilions, the white Lotus |
272 Flower Pagoda and the Suzhou-style gardens. One the way we would |
223 Flower Pagoda and the Suzhou-style gardens. |
273 visit the <A HREF="http://arts.cultural-china.com/en/85Arts6286.html">Daming Temple</A> |
|
274 and the old Stone Pagoda of Yangzhou. The day |
|
275 will finish with a dinner in the well-known |
|
276 <A HREF="http://en.wikipedia.org/wiki/Fuchun_Teahouse">Fuchun</A> restaurant. |
|
277 |
|
278 <center> |
224 <center> |
279 <table style="width: 75%"> |
225 <table style="width: 75%"> |
280 <tr> |
226 <tr> |
281 <td> |
227 <td> |
282 <img src="pics/Yangzhou2.jpg" alt="Yangzhou" width="98%" height="21%" border=0> |
228 <img src="pics/Yangzhou2.jpg" alt="Yangzhou" width="98%" height="21%" border=0> |