Mercurial Mercurial > hg > itp-2015 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
index.html
changeset 86 99f336f35f87
parent 84 2e2e4680a9d2
child 87 c8156c1b463c
equal deleted inserted replaced
85:2312c316736d 86:99f336f35f87 
   113 </TABLE>
 
   113 </TABLE>
 
   114 <p>
 
   114 <p>
 
   115 <HR>
 
   115 <HR>
 
   116 [<a href="index.html#dates">Important Dates</a>]
 
   116 [<a href="index.html#dates">Important Dates</a>]
 
   117 [<A HREF="cfp.pdf">CFP</A>]
 
   117 [<A HREF="cfp.pdf">CFP</A>]
 
       
   118 [<a href="index.html#committees">Committees</a>]
 
   118 [<A HREF="history.html">Conference History</A>]
 
   119 [<A HREF="history.html">Conference History</A>]
 
   119 <HR></p>
 
   120 <HR></p>
 
   120 
   121 
   121 <p>
 
   122 <p>
 
   122 The 6th conference on Interactive Theorem Proving will be held in
 
   123 The 6th conference on Interactive Theorem Proving will be held in
 
   129 We expect to have more information about travelling and a detailed programme
 
   130 We expect to have more information about travelling and a detailed programme
 
   130 nearer the time. The proceedings will be published as usual in the LNCS
 
   131 nearer the time. The proceedings will be published as usual in the LNCS
 
   131 Series.
 
   132 Series.
 
   132 </p>
 
   133 </p>
 
   133 
   134 
   134 <H3><A NAME="dates"></A>Important Dates</H3>
 
   135 <p>
 
       
   136 <IMG SRC="pics/new.gif" ALT="" style="" align="left">There will be an Isabelle tutorial before the
 
       
   137 conference (21 - 23 August), and<BR><BR>
 
       
   138 <IMG SRC="pics/new.gif" ALT="" style="" align="left">there will be a Coq tutorial after the conference
 
       
   139 (27 - 29 August).<BR><BR>
 
       
   140 </p>
 
       
   141 
       
   142 <H4><A NAME="dates"></A>Important Dates</H4>
 
       
   143 
   135 Submission of title and abstracts: 9 March 2015<BR>
 
   144 Submission of title and abstracts: 9 March 2015<BR>
 
   136 Submission of full papers: 13 March 2015<BR>
 
   145 Submission of full papers: 13 March 2015<BR>
 
   137 Author notification: 15 May 2015<BR>
 
   146 Author notification: 15 May 2015<BR>
 
   138 Camera-ready papers: 5 June 2015<BR>
 
   147 Camera-ready papers: 5 June 2015<BR>
 
   139 Conference: 14-27 August 2015<BR>
 
   148 Conference: 14-27 August 2015<BR>
 
   140 
   149 
   141 <H4>Timing and Tentative Programme</H4>
 
   150 <H4>Tentative Programme</H4>
 
   142 
   151 
   143 The conference will be held in the last week of August (24th - 27th
 
   152 The conference will be held in the last week of August (24th - 27th
 
   144 August 2015).  As is the tradition, the conference consists of 4 days
 
   153 August 2015).  As is the tradition, the conference consists of 4 days
 
   145 of research presentations and invited talks. Like in previous
 
   154 of research presentations and invited talks. Like in previous
 
   146 conferences, we would allow ample time between the formal sessions for
 
   155 conferences, we would allow ample time between the formal sessions for
 
   147 attendees to mingle and converse. Half a day will be dedicated to an
 
   156 attendees to mingle and converse. Half a day will be dedicated to an
 
   148 excursion.
 
   157 excursion.
 
   149 
   158 
   150 <p>
 
   159 <H4><A NAME="committees"></A>Committees</H4>
 
   151 <IMG SRC="pics/new.gif" ALT="" style="" align="left">There will be an Isabelle tutorial before the
 
   160 
   152 conference (21 - 23 August), and<BR><BR>
 
   161 <H5>Programme Committee:</H5>
 
   153 <IMG SRC="pics/new.gif" ALT="" style="" align="left">there will be a Coq tutorial after the conference
 
   162 
   154 (27 - 29 August).<BR><BR>
 
   163 <TABLE>
 
   155 </p>
 
   164 <TR><TD><A HREF="http://www.cs.unibo.it/~asperti/">Andrea Asperti</A></TD>
 
       
   165     <TD>University of Bologna, Italy</TD>
 
       
   166 </TR>
 
       
   167 <TR><TD><A HREF="http://www.itu.dk/people/jebe/">Jesper Bengtson</A></TD>
 
       
   168     <TD>IT University of Copenhagen, Denmark</TD>
 
       
   169 </TR>
 
       
   170 <TR><TD><A HREF="http://wwwbroy.in.tum.de/~berghofe/">Stefan Berghofer</A></TD>
 
       
   171     <TD>Secunet Security Networks AG, Germany</TD>
 
       
   172 </TR>
 
       
   173 <TR><TD><A HREF="http://www-sop.inria.fr/members/Yves.Bertot/">Yves Bertot</A></TD>
 
       
   174     <TD>INRIA, France</TD>
 
       
   175 </TR>
 
       
   176 <TR><TD><A HREF="http://cs.au.dk/~birke/">Lars Birkedal</A></TD>
 
       
   177     <TD>Aarhus University, Denmark</TD>
 
       
   178 </TR>
 
       
   179 <TR><TD><A HREF="http://www.cse.chalmers.se/~coquand/">Thierry Coquand</A></TD>
 
       
   180     <TD>University of Gothenburg, Sweden</TD>
 
       
   181 </TR>
 
       
   182 <TR><TD><A HREF="http://staff.ustc.edu.cn/~xyfeng/">Xinyu Feng</A></TD>
 
       
   183     <TD>University of Science and Technology, China</TD>
 
       
   184 </TR>
 
       
   185 <TR><TD><A HREF="http://www.cs.uwyo.edu/~ruben/">Ruben Gamboa</A></TD>
 
       
   186     <TD>University of Wyoming, USA</TD>
 
       
   187 </TR>
 
       
   188 <TR><TD><A HREF="http://www.cs.ru.nl/~herman/">Herman Geuvers</A></TD>
 
       
   189     <TD>Radboud University Nijmegen, The Netherlands</TD>
 
       
   190 </TR>
 
       
   191 <TR><TD><A HREF="http://www.cl.cam.ac.uk/~mjcg/">Mike Gordon</A></TD>
 
       
   192     <TD>Cambridge University, United Kingdom</TD>
 
       
   193 </TR>
 
       
   194 <TR><TD><A HREF="http://web.engr.illinois.edu/~egunter/">Elsa Gunter</A></TD>
 
       
   195     <TD>University of Illinois, Urbana-Champaign, USA</TD>
 
       
   196 </TR>
 
       
   197 <TR><TD><A HREF="http://www.cl.cam.ac.uk/~jrh13/">John Harrison</A></TD>
 
       
   198     <TD>Intel Corporation, USA</TD>
 
       
   199 </TR>
 
       
   200 <TR><TD><A HREF="http://pauillac.inria.fr/~herbelin/index-eng.html">Hugo Herbelin</A></TD>
 
       
   201     <TD>INRIA, France</TD>
 
       
   202 </TR>
 
       
   203 <TR><TD><A HREF="http://www.cs.utexas.edu/~kaufmann/">Matt Kaufmann</A></TD>
 
       
   204     <TD>University of Texas at Austin, USA</TD>
 
       
   205 </TR>
 
       
   206 <TR><TD><A HREF="http://www.cse.unsw.edu.au/~kleing/">Gerwin Klein</A></TD>
 
       
   207     <TD>NICTA, Australia</TD>
 
       
   208 </TR>
 
       
   209 <TR><TD><A HREF="http://shemesh.larc.nasa.gov/people/cam/">C&#233;sar Mu&#241;oz</A></TD>
 
       
   210     <TD>NASA Langley Research Center, USA</TD>
 
       
   211 </TR>
 
       
   212 <TR><TD><A HREF="http://www21.in.tum.de/~nipkow/">Tobias Nipkow</A></TD>
 
       
   213     <TD>TU M&uuml;nchen, Germany</TD>
 
       
   214 </TR>
 
       
   215 <TR><TD><A HREF="http://nicta.com.au/people/norrishm">Michael Norrish</A></TD>
 
       
   216     <TD>NICTA, Australia</TD>
 
       
   217 </TR>
 
       
   218 <TR><TD><A HREF="http://www.cs.kent.ac.uk/people/staff/sao/">Scott Owens</A></TD>
 
       
   219     <TD>University of Kent, United Kingdom</TD>
 
       
   220 </TR>
 
       
   221 <TR><TD><A HREF="http://homepages.inf.ed.ac.uk/rpollack/">Randy Pollack</A></TD>
 
       
   222     <TD>Havard University, USA</TD>
 
       
   223 </TR>
 
       
   224 <TR><TD><A HREF="http://www.itu.dk/people/carsten/">Carsten Sch&uuml;rmann</A></TD>
 
       
   225     <TD>IT University of Copenhagen, Denmark</TD>
 
       
   226 </TR>
 
       
   227 <TR><TD>Konrad Slind</TD>
 
       
   228     <TD>Rockwell Collins, USA</TD>
 
       
   229 </TR>
 
       
   230 <TR><TD><A HREF="http://www.ntu.edu.sg/home/atiu/">Alwen Tiu</A></TD>
 
       
   231     <TD>Nanyang Technological University, Singapore</TD>
 
       
   232 </TR>
 
       
   233 <TR><TD><A HREF="http://www.inf.kcl.ac.uk/staff/urbanc/">Christian Urban</A> (co-chair)&nbsp;</TD>
 
       
   234     <TD>(King's College London, United Kingdom</TD>
 
       
   235 </TR>
 
       
   236 <TR><TD><A HREF="http://research.microsoft.com/en-us/people/dimitris/">Dimitrios Vytiniotis</A></TD>
 
       
   237     <TD>Microsoft Research Cambridge, United Kingdom</TD>
 
       
   238 </TR>
 
       
   239 <TR><TD>Xingyuan Zhang (co-chair)</TD>
 
       
   240     <TD>PLA University of Science and Technology, China</TD>
 
       
   241 </TR>
 
       
   242 </TABLE>
 
   156 
   243 
   157 <H4>Travel to Nanjing</H4>
 
   244 <H4>Travel to Nanjing</H4>
 
   158 
   245 
   159 Nanjing is a major city in China.  There are international airline
 
   246 Nanjing is a major city in China.  There are international airline
 
   160 connections directly to <A
 
   247 connections directly to <A
 
   206 
   293 
   207 There are also many additional
 
   294 There are also many additional
 
   208 <A HREF="http://wikitravel.org/en/Nanjing#Sleep">hotels</A> in all price categories nearby.
 
   295 <A HREF="http://wikitravel.org/en/Nanjing#Sleep">hotels</A> in all price categories nearby.
 
   209 
   296 
   210 
   297 
   211 <H4>Advantages of Hosting ITP in Nanjing</H4>
 
   298 <H4>Local Information</H4>
 
   212 
   299 
   213 There are several groups in the ITP area that are active in China. For example for the last
 
   300 There are several groups in the ITP area that are active in China. For example for the last
 
   214 five years there have been popular
 
   301 five years there have been popular
 
   215 <A HREF="http://sts.thss.tsinghua.edu.cn/APSSFM_2013">summerschools</A> in China about Coq
 
   302 <A HREF="http://sts.thss.tsinghua.edu.cn/APSSFM_2013">summerschools</A> in China about Coq
 
   216 with 50 or so student participants each. ITP (and TPHOLs) have
 
   303 with 50 or so student participants each. ITP (and TPHOLs) have
 
   278 <H4>Finance</H4>
 
   365 <H4>Finance</H4>
 
   279 
   366 
   280 We will seek to keep costs low by negotiating discounts with
 
   367 We will seek to keep costs low by negotiating discounts with
 
   281 the hotel and by trying to find sponsoring where sensible.  
   368 the hotel and by trying to find sponsoring where sensible.  
   282 
   369 
   283 <H4>Experience of the Programme Chairs and Local Organisation</H4>
 
       
   284 
       
   285 Xingyuan and Christian are regular participants at ITP. Christian was a
 
       
   286 co-organiser of the TPHOLs conference
 
       
   287 in 2009 in <A HREF="http://isabelle.in.tum.de/nominal/activities/tphols09/">Munich</A>.
 
       
   288 We will make use of the infrastructure available at Xingyuan's university for local
 
       
   289 organisation. There will also be a student team that helps with running the conference.
 
       
   290 </TD>
 
   370 </TD>
 
   291 </TR>
 
   371 </TR>
 
   292 </TABLE>
 
   372 </TABLE>
 
   293 
   373 
   294 <hr>
 
   374 <hr>
itp-2015