<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"><html><head><title>ITP 2015 in Nanjing</title><meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1"> <style type="text/css"> #map_canvas { width: 500px; height: 400px; } </style> <script type="text/javascript" src="https://maps.googleapis.com/maps/api/js?sensor=false"></script> <script type="text/javascript"> function initialize() { var Latlng = new google.maps.LatLng(32.060255, 118.796877); var map_canvas = document.getElementById('map_canvas'); var map_options = { center: Latlng, zoom: 0, mapTypeId: google.maps.MapTypeId.HYBRID } var map = new google.maps.Map(map_canvas, map_options) var marker = new google.maps.Marker({ position: Latlng, map: map, title: 'Nanjing' }); } google.maps.event.addDomListener(window, 'load', initialize); </script><style type="text/css"> body { font-family: "trebuchet ms", helvetica, sans-serif; }</style></head><BODY TEXT="#000000" BGCOLOR="#4169E1" LINK="#0000EF" VLINK="#51188E" ALINK="#FF0000" onload="initialize()" onunload="GUnload()"><TABLE WIDTH="100%" BGCOLOR="#4169E1" BORDER="0" FRAME="border" CELLPADDING="10" CELLSPACING="2" RULES="all"><!-- left column --><TR><TD BGCOLOR="#FFFFFF" WIDTH="20%" VALIGN="TOP" ROWSPAN="2"><p align=center><a href="pics/ITP-Linggusu.jpg"><img src="pics/ITP-Linggusu.jpg" width="50%" height="12%" alt="Linggusi" border=0></a><br>Linggusi pagoda<br></p><p align=center><a href="pics/ITP-Mochou.jpg"><img src="pics/ITP-Mochou.jpg" alt="Mochou" width="88%" height="18%" border=0></a><br>Mochou Lake Park<br></p><p align=center><a href="pics/ITP-najing-cit-walk.jpg"><img src="pics/ITP-najing-cit-walk.jpg" alt="City Wall" width="50%" height="18%" border=0></a><br>Nanjing city wall<br></p><p align=center><a href="pics/Nanjing2.jpg"><img src="pics/Nanjing2.jpg" alt="City Wall" width="80%" height="13%" border=0></a><br>`"Elephant Road" of the<br> Ming tomb<br></p><p align=center><a href="pics/Nanjing3.jpg"><img src="pics/Nanjing3.jpg" alt="Nanjing's skyline" width="80%" height="13%" border=0></a><br>Nanjing's skyline<br></p><p align=center><a href="pics/Nanjing4.jpg"><img src="pics/Nanjing4.jpg" alt="Science and Technology Museum" width="80%" height="18%" border=0></a><br>Science and Technology<br> Museum<br></p> </TD><!-- right column --><TD BGCOLOR="#FFFFFF" WIDTH="75%" VALIGN="TOP"><TABLE><TR><TD><H1>ITP 2015 will be in Nanjing, China</H1></TD><TD align="right" valign="top"><img src="pics/nanjing-map.jpg" width="42%" height="40%" alt="ITP" align="top"></TD></TR></TABLE><p><HR>[<A HREF="index.html#dates">Important Dates</A>][<A HREF="index.html#programme">Programme</A>][<A HREF="index.html#travel">Travel + Registration</A>][<A HREF="http://talisker.inf.kcl.ac.uk/%7Eurbanc/cgi-bin/repos.cgi/itp-2015/raw-file/tip/booklet.pdf">ITP Booklet</A>]<BR>[<A HREF="accepted.html">Accepted Papers</A>][<A HREF="cfp.pdf">CFP</A>][<A HREF="index.html#committees">Committees</A>][<A HREF="history.html">Conference History</A>][<A HREF="bids-2016.html">ITP 2016 Bids</A>]<HR><p>The 6th conference on Interactive Theorem Proving will be held inNanjing, China. <A HREF="http://en.wikipedia.org/wiki/Nanjing">Nanjing</A> is situatedin the heart of China — close to Shanghai and roughlyequidistant between Beijing and Hong Kong. It is a former capitalduring the Ming Dynasty with a rich <AHREF="http://www.cityofnanjing.com">cultural heritage</A>. The proceedings will be published as usual in the LNCSSeries. There will be an<A HREF="http://www21.in.tum.de/~nipkow/isa-tut-itp15.html">Isabelle tutorial</A> before theconference (21 - 23 August), anda <A HREF="http://www.strub.nu/coq-itp-15">Coq tutorial</A> after the conference(27 - 29 August).<p><IMG SRC="pics/new.gif" ALT="" style="" align="left"><A HREF=""http://talisker.inf.kcl.ac.uk/%7Eurbanc/cgi-bin/repos.cgi/itp-2015/raw-file/tip/prog.pdf">Preliminary programme</A><BR><BR><IMG SRC="pics/new.gif" ALT="" style="" align="left"><A HREF="http://talisker.inf.kcl.ac.uk/%7Eurbanc/cgi-bin/repos.cgi/itp-2015/raw-file/tip/booklet.pdf">ITP Booklet</A>,contains practical information about registration, travelling, etc.<BR><BR></p><H4><A NAME="dates"></A>Important Dates</H4>Submission of title and abstracts: 9 March 2015<BR>Submission of full papers: <strike>13 March 2015</strike> 20 March 2015<font color="red">closed</font><BR>Author notification: 15 May 2015<BR>Camera-ready papers: 5 June 2015<BR>Conference: 24-27 August 2015<BR><A HREF="https://easychair.org/conferences/?conf=itp2015">Submission page</A><BR><H4><A NAME="programme">Tentative Programme</H4>As is the tradition, the conference consists of 4 daysof research presentations and invited talks. Like in previousconferences, we will have ample time between the formal sessions forattendees to mingle and converse. Half a day will be dedicated to anexcursion to <A HREF="http://en.wikipedia.org/wiki/Yangzhou">Yangzhou</A>and the <A HREF="http://en.wikipedia.org/wiki/Yangzhou#Slender_West_Lake">Slender West Lake</A>.The preliminary programme of talks can be found<A HREF="http://talisker.inf.kcl.ac.uk/%7Eurbanc/cgi-bin/repos.cgi/itp-2015/raw-file/tip/prog.pdf">here</A>.<H4><A NAME="travel">Travel to Nanjing</H4>Nanjing is a major city in China. There are international airlineconnections directly to <AHREF="http://en.wikipedia.org/wiki/Nanjing_Lukou_International_Airport">NanjingLukou Airport</A> and via transfer at airports in Hong Kong, Beijing,Shanghai and many others. There are also very convenient trainconnections from Shanghai and Beijing, which take slightly more than1h from Shanghai and about 4h from Beijing. Travel within Nanjing canbe done cheaply via taxi and public transport. Hopefully helpful tipsfor travelling in Nanjing and China can be found in the<A HREF="http://talisker.inf.kcl.ac.uk/%7Eurbanc/cgi-bin/repos.cgi/itp-2015/raw-file/tip/booklet.pdf">booklet</A>.<p>Remember that travelling to China requires a<A HREF="http://www.travelchinaguide.com/embassy/visa.htm">visa</A>;but it should be relatively easy to obtain one for participants. You will needa letter of invitation which Chunhan will send you (chunhanwu at 126 dot com).You need to provide him with your name, title, DOB, work address, e-mail and paper title(if you present a paper). See the <A HREF="http://talisker.inf.kcl.ac.uk/%7Eurbanc/cgi-bin/repos.cgi/itp-2015/raw-file/tip/booklet.pdf">booklet</A> fordetails about the visa application.<p><center><div id="map_canvas" style="width: 300px; height: 170px"></div></center><H4>Registration</H4>The early rate of the registration fee will be 3300元 (ca. £350/$533/€488).The late rate starting from 1 August will be 3800元.The registration fee includes lunches during theconference. It also covers the excursion, the conference banquet and a welcome reception.The tutorials are separate. Their registration fee is 250元 for the Isabelle-tutorialand 200元 for the Coq-tutorial.<p>The registration fee needs to be transferred via a banktransfer; we <span style="text-decoration: underline;"><B>cannot</B></span>accept credit cards etc for the conference fee. The hotel and many other things can be paidby credit card, but not the conference fee. See the <A HREF="booklet.pdf">booklet</A> fordetails about the bank transfer.<H4>Venue and Accommodation</H4>The conference will take place at the<A HREF="http://english.ctrip.com/hotels/nanjing-hotel-detail-66456/nanjing-hanyuan-mansion-center-of-academic-exchange/">HanyuanHotel</A>, which is relatively inexpensive(ca. 390元/£34/$52/€47 per night including breakfast)and in easy reach from the city centre (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>at Google Maps). The conference hotel has the usual amenities (Wifi, conference rooms, etc)and includes a restaurant. We have reserved some rooms in the hotel for participants. See the<A HREF="booklet.pdf">booklet</A> for information about the hotel booking.<p><center><table style="width: 75%"><tr><td><img src="pics/hotel1.jpg" alt="hotel" width="98%" height="21%" border=0></td><td><img src="pics/hotel2.jpg" alt="hotel" width="98%" height="21%" border=0></td><td><img src="pics/hotel4.jpg" alt="hotel" width="98%" height="21%" border=0></td></tr><tr><td colspan="3"><center><small>Hanyuan Hotel</small></center></td> </tr> </table></center><p>There are also many additional<A HREF="http://wikitravel.org/en/Nanjing#Sleep">hotels</A> in all price categories nearby.Also there are innumerable <AHREF="http://www.chinatour.com/nanjing/nanjing-food.htm">restaurants</A> in the area.<H4>Local Information</H4><p>Being in China, Nanjing offers the usual conveniences of good andaffordable food. It has several excellent<A HREF="http://en.wikipedia.org/wiki/Nanjing#Museums">museums</A>and tourist <A HREF="http://en.wikipedia.org/wiki/Nanjing#Tourism">attractions</A>.In the nearby vicinity are touristic hotspots like<A HREF="http://en.wikipedia.org/wiki/Yangzhou">Yangzhou</A>,<A HREF="http://en.wikipedia.org/wiki/Hangzhou">Hangzhou</A>,<A HREF="http://en.wikipedia.org/wiki/Wuxi">Wuxi</A> and<A HREF="http://en.wikipedia.org/wiki/Suzhou">Suzhou</A>.If you want to explore Nanjing yourself, the best tour is to go to the<A HREF="http://en.wikipedia.org/wiki/Purple_Mountain">Purple Mountains</A> passing bythe <A HREF="http://en.wikipedia.org/wiki/Linggu_Temple">Linggusi</A> pagoda,the <A HREF="http://en.wikipedia.org/wiki/City_Wall_of_Nanjing">city wall</A> and the<A HREF="http://en.wikipedia.org/wiki/Ming_Xiaoling_Mausoleum">Ming tombs</A> (see pictures onthe left). There is a wide selection of excellent restaurants aroundNanjing's Confucius Temple. <H4>Excursion</H4>The excursion will be to <A HREF="http://en.wikipedia.org/wiki/Yangzhou">Yangzhou</A> (1h awayfrom Nanjing by bus). The tour will include a walkaround the Slender West Lake with its pavilions, the white LotusFlower Pagoda and the Suzhou-style gardens. One the way we wouldvisit the <A HREF="http://arts.cultural-china.com/en/85Arts6286.html">Daming Temple</A>and the old Stone Pagoda of Yangzhou. The daywill finish with a dinner in the well-known<A HREF="http://en.wikipedia.org/wiki/Fuchun_Teahouse">Fuchun</A> restaurant.<center><table style="width: 75%"><tr><td><img src="pics/Yangzhou2.jpg" alt="Yangzhou" width="98%" height="21%" border=0></td><td><img src="pics/Yangzhou1.jpg" alt="Yangzhou" width="98%" height="21%" border=0></td><td><img src="pics/Yangzhou3.jpg" alt="Yangzhou" width="98%" height="21%" border=0></td></tr><tr><td colspan="3"><center><small>Yangzhou, Slender West Lake</small></center></td> </tr> </table></center><H4><A NAME="committees"></A>Programme Committee</H4><TABLE><TR><TD><A HREF="http://www.cs.unibo.it/~asperti/">Andrea Asperti</A></TD> <TD>University of Bologna, Italy</TD></TR><TR><TD><A HREF="http://www.itu.dk/people/jebe/">Jesper Bengtson</A></TD> <TD>IT University of Copenhagen, Denmark</TD></TR><TR><TD><A HREF="http://wwwbroy.in.tum.de/~berghofe/">Stefan Berghofer</A></TD> <TD>Secunet Security Networks AG, Germany</TD></TR><TR><TD><A HREF="http://www-sop.inria.fr/members/Yves.Bertot/">Yves Bertot</A></TD> <TD>INRIA, France</TD></TR><TR><TD><A HREF="http://cs.au.dk/~birke/">Lars Birkedal</A></TD> <TD>Aarhus University, Denmark</TD></TR><TR><TD><A HREF="https://www.irisa.fr/celtique/blazy/index.html">Sandrine Blazy</A></TD> <TD>University of Rennes, France</TD></TR><TR><TD><A HREF="http://www.cs.cornell.edu/home/rc/">Bob Constable</A></TD> <TD>Cornell University, USA</TD></TR><TR><TD><A HREF="http://www.cse.chalmers.se/~coquand/">Thierry Coquand</A></TD> <TD>University of Gothenburg, Sweden</TD></TR><TR><TD><A HREF="http://staff.ustc.edu.cn/~xyfeng/">Xinyu Feng</A></TD> <TD>University of Science and Technology, China</TD></TR><TR><TD><A HREF="http://www.cs.uwyo.edu/~ruben/">Ruben Gamboa</A></TD> <TD>University of Wyoming, USA</TD></TR><TR><TD><A HREF="http://www.cs.ru.nl/~herman/">Herman Geuvers</A></TD> <TD>Radboud University Nijmegen, The Netherlands</TD></TR><TR><TD><A HREF="http://www.cl.cam.ac.uk/~mjcg/">Mike Gordon</A></TD> <TD>Cambridge University, United Kingdom</TD></TR><TR><TD><A HREF="http://web.engr.illinois.edu/~egunter/">Elsa Gunter</A></TD> <TD>University of Illinois, Urbana-Champaign, USA</TD></TR><TR><TD><A HREF="http://www.cl.cam.ac.uk/~jrh13/">John Harrison</A></TD> <TD>Intel Corporation, USA</TD></TR><TR><TD><A HREF="http://pauillac.inria.fr/~herbelin/index-eng.html">Hugo Herbelin</A></TD> <TD>INRIA, France</TD></TR><TR><TD><A HREF="http://www.cs.utexas.edu/~kaufmann/">Matt Kaufmann</A></TD> <TD>University of Texas at Austin, USA</TD></TR><TR><TD><A HREF="http://www.cse.unsw.edu.au/~kleing/">Gerwin Klein</A></TD> <TD>NICTA, Australia</TD></TR><TR><TD><A HREF="http://shemesh.larc.nasa.gov/people/cam/">César Muñoz</A></TD> <TD>NASA Langley Research Center, USA</TD></TR><TR><TD><A HREF="http://www21.in.tum.de/~nipkow/">Tobias Nipkow</A></TD> <TD>TU München, Germany</TD></TR><TR><TD><A HREF="http://nicta.com.au/people/norrishm">Michael Norrish</A></TD> <TD>NICTA, Australia</TD></TR><TR><TD><A HREF="http://www.cs.kent.ac.uk/people/staff/sao/">Scott Owens</A></TD> <TD>University of Kent, United Kingdom</TD></TR><TR><TD><A HREF="http://homepages.inf.ed.ac.uk/rpollack/">Randy Pollack</A></TD> <TD>Harvard University, USA</TD></TR><TR><TD><A HREF="http://www.itu.dk/people/carsten/">Carsten Schürmann</A></TD> <TD>IT University of Copenhagen, Denmark</TD></TR><TR><TD><A HREF="http://loonwerks.com/people/konrad-slind.html">Konrad Slind</A></TD> <TD>Rockwell Collins, USA</TD></TR><TR><TD><A HREF="http://www.ntu.edu.sg/home/atiu/">Alwen Tiu</A></TD> <TD>Nanyang Technological University, Singapore</TD></TR><TR><TD><A HREF="http://www.inf.kcl.ac.uk/staff/urbanc/">Christian Urban</A> (co-chair) </TD> <TD>King's College London, United Kingdom</TD></TR><TR><TD><A HREF="http://research.microsoft.com/en-us/people/dimitris/">Dimitrios Vytiniotis</A></TD> <TD>Microsoft Research Cambridge, United Kingdom</TD></TR><TR><TD>Xingyuan Zhang (co-chair)</TD> <TD>PLA University of Science and Technology, China</TD></TR></TABLE><H4>Finance</H4>We are grateful for the generous support received from the PLA University ofScience and Technology in Nanjing.</TD></TR></TABLE><hr><a href="http://validator.w3.org/check/referer">[Validate this page.]</a></body></html>