<!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="cfp.pdf">CFP</A>]+ −
[<A HREF="index.html#committees">Committees</A>]+ −
[<A HREF="history.html">Conference History</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>. + −
We expect to have more information about travelling and a detailed programme+ −
nearer the time. The proceedings will be published as usual in the LNCS+ −
Series.+ −
</p>+ −
+ − <p>+ −
<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 Coq tutorial 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: 13 March 2015<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>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.+ −
+ − <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>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>+ −
<center>+ −
<div id="map_canvas" style="width: 300px; height: 170px"></div>+ −
</center>+ −
+ − <H4>Venue and Accommodation</H4>+ −
+ − The plan is to host the conference 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 inexpensive+ −
(ca. 350元/£35/$60/€40 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). It has the usual amenities for hosting conferences+ −
(Wifi, conference rooms, etc) and has links to neighbouring+ −
universities. There is also the possibility to use lecture rooms for+ −
free in Xingyuan's university at the other side of the road. 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.+ −
+ − <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>+ −
+ − There are also many additional+ −
<A HREF="http://wikitravel.org/en/Nanjing#Sleep">hotels</A> in all price categories nearby.+ −
+ − + − <H4>Local Information</H4>+ −
+ − 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.+ −
+ − <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>.+ −
Travelling+ −
<A HREF="http://www.travelchinaguide.com/embassy/visa.htm">visas</A>+ −
to China should be easy to obtain for participants.+ −
+ − + − <H4>Excursion</H4>+ −
+ − We have two possible destinations for an excursion in mind: one is to+ −
<A HREF="http://en.wikipedia.org/wiki/Yangzhou">Yangzhou</A> (1h away+ −
from Nanjing by bus), and the other is a (more leisurely) tour of+ −
Nanjing and its attractions. The tour to Yangzhou would involve 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+ −
would finish with a dinner in the well-known+ −
<A HREF="http://en.wikipedia.org/wiki/Fuchun_Teahouse">Fuchun</A> restaurant. The+ −
best tour around Nanjing 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 for a conference dinner. We will canvas for opinions about+ −
what participants would be most interested in.+ −
+ − <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>Finance</H4>+ −
+ − We will seek to keep costs low by negotiating discounts with+ −
the hotel and by trying to find sponsoring where sensible. + −
+ − </TD>+ −
</TR>+ −
</TABLE>+ −
+ − <hr>+ −
<a href="http://validator.w3.org/check/referer">[Validate this page.]</a>+ −
</body>+ −
</html>+ −