<!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-size: 14px;
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="TUM" 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>]<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 in
Nanjing, China.
<A HREF="http://en.wikipedia.org/wiki/Nanjing">Nanjing</A> is situated
in the heart of China — close to Shanghai and roughly
equidistant between Beijing and Hong Kong. It is a former capital
during the Ming Dynasty with a rich <A
HREF="http://www.cityofnanjing.com">cultural heritage</A>.
The proceedings will be published as usual in the LNCS
Series.
<p>
There are several groups in the ITP area that are active in China. For example for the last
five years there have been popular
<A HREF="http://kyhcs.ustcsz.edu.cn/fmschool-2011">summerschools</A> in China about Coq
with 50 or so student participants each. ITPs (and TPHOLs) have
<A HREF="history.html">never</A> been hosted in
China, and this might be an opportunity for the ITP community to foster relations
with researchers from China and Asia, and for local researchers to become part of the
ITP community. We welcome everybody and hope participants will have a beneficial time at ITP 2015.
</p>
<p>
<IMG SRC="pics/new.gif" ALT="" style="" align="left"><A HREF="accepted.html">Accepted papers</A><BR><BR>
<IMG SRC="pics/new.gif" ALT="" style="" align="left">There will be an Isabelle tutorial before the
conference (21 - 23 August), and<BR><BR>
<IMG SRC="pics/new.gif" ALT="" style="" align="left">a
<A HREF="http://www.strub.nu/coq-itp-15">Coq tutorial</A> after the conference
(27 - 29 August).<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>
The conference will be held in the last week of August (24th - 27th
August 2015). As is the tradition, the conference consists of 4 days
of research presentations and invited talks. Like in previous
conferences, we will allow ample time between the formal sessions for
attendees to mingle and converse. Half a day will be dedicated to an
excursion 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 list of accepted papers can be found <A HREF="accepted.html">here</A>.
The more detailed programme will be posted soon.
<H4><A NAME="travel">Travel to Nanjing</H4>
Nanjing is a major city in China. There are international airline
connections directly to <A
HREF="http://en.wikipedia.org/wiki/Nanjing_Lukou_International_Airport">Nanjing
Lukou Airport</A> and via transfer at airports in Hong Kong, Beijing,
Shanghai and many others. There are also very convenient train
connections from Shanghai and Beijing, which take slightly more than
1h from Shanghai and about 4h from Beijing. Travel within Nanjing can
be done cheaply via taxi and public transport. We will post detailed travel
instructions nearer the time.
<p>
Remember that travelling to China requires
<A HREF="http://www.travelchinaguide.com/embassy/visa.htm">visas</A>,
but they should be relatively easy to obtain for participants. You will need
a letter of invitation which Xingyuan will send you (xingyuanzhang at 126 dot com).
You need to provide him with name, title, work address, e-mail and paper title
(if you present a paper).
<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 3500元 (ca. £370/$565/€530).
The late rate starting from 1 August will be 4000元.
The registration fee includes lunches and dinners during the
conference. It also covers the excursion, conference banquette and welcome reception. The
registration fee needs to be transferred via a bank
transfer; we <B>cannot</B> accept credit cards etc. We will send details about the registration
procedure soon.
<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/">Hanyuan
Hotel</A>, which is relatively inexpensive
(ca. 350元/£37/$57/€53 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). We have reserved rooms for participants and will soon
send details about the booking procedure. There are also many additional
<A HREF="http://wikitravel.org/en/Nanjing#Sleep">hotels</A> in all price categories nearby.
<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>
The conference hotel has the usual amenities (Wifi, conference rooms, etc).
Hanyuan Hotel includes a restaurant and there are innumerable <A
HREF="http://www.chinatour.com/nanjing/nanjing-food.htm">restaurants</A>
around the hotel and in downtown Nanjing, all usually very affordable.
<H4>Local Information</H4>
<p>
Being in China, Nanjing offers the usual conveniences of good and
affordable 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 by
the <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 on
the left). There is a wide selection of excellent restaurants around
Nanjing's Confucius Temple.
<H4>Excursion</H4>
The excursion will be to
<A HREF="http://en.wikipedia.org/wiki/Yangzhou">Yangzhou</A> (1h away
from Nanjing by bus). The tour will include a walk
around the Slender West Lake with its pavilions, the white Lotus
Flower Pagoda and the Suzhou-style gardens. One the way we would
visit the <A HREF="http://arts.cultural-china.com/en/85Arts6286.html">Daming Temple</A>
and the old Stone Pagoda of Yangzhou. The day
will 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 of
Science and Technology in Nanjing.
</TD>
</TR>
</TABLE>
<hr>
<a href="http://validator.w3.org/check/referer">[Validate this page.]</a>
</body>
</html>