115
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 2 <html>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 3 <head>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 4 <title>ITP 2015 in Nanjing</title>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 5 <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 6 <style type="text/css">
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 7 #map_canvas {
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 8 width: 500px;
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 9 height: 400px;
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 10 }
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 11 </style>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 12 <script type="text/javascript" src="https://maps.googleapis.com/maps/api/js?sensor=false"></script>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 13 <script type="text/javascript">
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 14 function initialize() {
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 15 var Latlng = new google.maps.LatLng(32.060255, 118.796877);
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 16 var map_canvas = document.getElementById('map_canvas');
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 17 var map_options = {
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 18 center: Latlng,
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 19 zoom: 0,
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 20 mapTypeId: google.maps.MapTypeId.HYBRID
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 21 }
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 22 var map = new google.maps.Map(map_canvas, map_options)
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 23
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 24 var marker = new google.maps.Marker({
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 25 position: Latlng,
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 26 map: map,
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 27 title: 'Nanjing'
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 28 });
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 29 }
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 30 google.maps.event.addDomListener(window, 'load', initialize);
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 31 </script>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 32 <style type="text/css">
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 33 body { font-size: 14px;
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 34 font-family: "trebuchet ms", helvetica, sans-serif; }
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 35 </style>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 36 </head>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 37
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 38 <BODY TEXT="#000000"
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 39 BGCOLOR="#4169E1"
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 40 LINK="#0000EF"
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 41 VLINK="#51188E"
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 42 ALINK="#FF0000"
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 43 onload="initialize()" onunload="GUnload()">
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 44
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 45 <TABLE WIDTH="100%"
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 46 BGCOLOR="#4169E1"
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 47 BORDER="0"
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 48 FRAME="border"
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 49 CELLPADDING="10"
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 50 CELLSPACING="2"
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 51 RULES="all">
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 52
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 53 <!-- left column -->
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 54 <TR>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 55 <TD BGCOLOR="#FFFFFF"
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 56 WIDTH="20%"
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 57 VALIGN="TOP"
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 58 ROWSPAN="2">
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 59
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 60
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 61 <p align=center>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 62 <a href="pics/ITP-Linggusu.jpg">
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 63 <img src="pics/ITP-Linggusu.jpg" width="50%" height="12%" alt="Linggusi" border=0></a>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 64 <br>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 65 Linggusi pagoda<br>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 66 </p>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 67
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 68 <p align=center>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 69 <a href="pics/ITP-Mochou.jpg">
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 70 <img src="pics/ITP-Mochou.jpg" alt="Mochou" width="88%" height="18%" border=0></a>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 71 <br>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 72 Mochou Lake Park<br>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 73 </p>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 74
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 75 <p align=center>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 76 <a href="pics/ITP-najing-cit-walk.jpg">
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 77 <img src="pics/ITP-najing-cit-walk.jpg" alt="City Wall" width="50%" height="18%" border=0></a>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 78 <br>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 79 Nanjing city wall<br>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 80 </p>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 81
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 82 <p align=center>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 83 <a href="pics/Nanjing2.jpg">
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 84 <img src="pics/Nanjing2.jpg" alt="City Wall" width="80%" height="13%" border=0></a>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 85 <br>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 86 "Elephant Road" of the<br> Ming tomb<br>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 87 </p>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 88
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 89 <p align=center>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 90 <a href="pics/Nanjing3.jpg">
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 91 <img src="pics/Nanjing3.jpg" alt="Nanjing's skyline" width="80%" height="13%" border=0></a>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 92 <br>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 93 Nanjing's skyline<br>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 94 </p>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 95
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 96 <p align=center>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 97 <a href="pics/Nanjing4.jpg">
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 98 <img src="pics/Nanjing4.jpg" alt="Science and Technology Museum" width="80%" height="18%" border=0></a>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 99 <br>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 100 Science and Technology<br> Museum<br>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 101 </p>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 102
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 103 </TD>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 104
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 105
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 106 <!-- right column -->
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 107 <TD BGCOLOR="#FFFFFF" WIDTH="75%" VALIGN="TOP">
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 108 <TABLE>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 109 <TR>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 110 <TD><H1>ITP Heritage and Conference History</H1></TD>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 111 </TABLE>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 112 <p>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 113 <HR>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 114 [<A HREF="index.html">Home</A>]
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 115 [<A HREF="index.html#dates">Important Dates</A>]
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 116 [<A HREF="cfp.pdf">CFP</A>]
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 117 [<A HREF="index.html#committees">Committees</A>]
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 118 [<A HREF="history.html">Conference History</A>]
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 119 <HR>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 120 </p>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 121
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 122 <p>ITP 2015 is the sixth conference on Interactive Theorem Proving and
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 123 related topics, ranging from theoretical foundations to implementation
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 124 aspects and applications in program verification, security, and
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 125 formalization of mathematics. The inaugural meeting of ITP was held on
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 126 11-14 July 2010 in Edinburgh, Scotland, as part of the Federated Logic
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 127 Conference (FLoC, 9-21 July 2010). ITP is the evolution of the TPHOLs
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 128 conference series to the broad field of interactive theorem
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 129 proving. TPHOLs meetings took place every year from 1988 until 2009.
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 130 </p>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 131
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 132 <h3>The TPHOLs conference series</h3>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 133
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 134 <p>TPHOLs 2009 was the twenty-second in a series of international
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 135 conferences on the applications of higher order logic theorem proving.
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 136 The first three (two at Cambridge and one at Århus) were informal
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 137 users' meetings for the HOL system and were the only ones without
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 138 published papers. Between 1991 and 1995 (Davis, Leuven, Vancouver,
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 139 Malta, Utah) the conference entertained an increasingly wide field of
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 140 interest. </p>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 141
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 142 <p>The evolution resulted in the program committee for the meeting in
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 143 Turku (1996) deeming that the scope of the conference included all
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 144 reasoning tools for higher order logics and adopted the name TPHOLs,
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 145 being an acronym for Theorem Proving in Higher Order Logics. (The
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 146 final letter being considered necessary to break the direct connection
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 147 between the conference and the HOL system.) This decision was strongly
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 148 endorsed at the business sessions at Turku and Murray Hill (1997).
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 149 </p>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 150
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 151 <p>An extensive collection of links to various aspects of previous
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 152 conferences in the series may be found below. </p>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 153
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 154 <h3>Associated communities</h3>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 155 <p>An inspection of the proceedings of recent conferences show that the conference accommodates the user communities of a number of theorem proving systems that support higher order logics. The interested reader is referred to the web sites for the following provers:<br>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 156
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 157 <a class='urllink' href='http://abella.cs.umn.edu' rel='nofollow'>Abella</a> -
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 158 <a class='urllink' href='http://wiki.portal.chalmers.se/agda/pmwiki.php' rel='nofollow'>Agda</a> -
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 159 <a class='urllink' href='http://www.cs.utexas.edu/users/moore/acl2' rel='nofollow'>ACL2</a> -
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 160 <a class='urllink' href='http://coq.inria.fr' rel='nofollow'>Coq</a> -
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 161 <a class='urllink' href='http://www.cl.cam.ac.uk/research/hvg/HOL' rel='nofollow'>HOL</a> -
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 162 <a class='urllink' href='http://imps.mcmaster.ca' rel='nofollow'>IMPS</a> -
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 163 <a class='urllink' href='http://www.cl.cam.ac.uk/research/hvg/Isabelle' rel='nofollow'>Isabelle</a> -
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 164 <a class='urllink' href='http://www.dcs.ed.ac.uk/home/lego' rel='nofollow'>LEGO</a> -
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 165 <a class='urllink' href='http://matita.cs.unibo.it' rel='nofollow'>Matita</a> -
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 166 <a class='urllink' href='http://www.nuprl.org' rel='nofollow'>Nuprl</a> -
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 167 <a class='urllink' href='http://www.lemma-one.com/ProofPower/index/index.html' rel='nofollow'>ProofPower</a> -
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 168 <a class='urllink' href='http://pvs.csl.sri.com' rel='nofollow'>PVS</a> -
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 169 </p>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 170
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 171 <h3>Traditions</h3>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 172
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 173 <p>A longstanding convention is that the annual conference should be
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 174 held in a continent different to the location of the previous meeting.
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 175 Another tradition is that the organizers for each meeting handle all
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 176 aspects of the conference for the whole year in consultation with the
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 177 previous few organizers. This includes selection of the programme
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 178 committee, editing the proceedings, fund-raising, programme and local
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 179 arrangements. Another responsibility of the organizers in year n is to
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 180 call for bids and conduct a poll for the selection of the venue for
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 181 the conference in year n+1. </p>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 182
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 183 <h3>ITP and TPHOLs conferences</h3>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 184
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 185 <table border='1'>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 186 <tr><td >2014</td><td ><a class='urllink' href='http://www.cs.uwyo.edu/~ruben/itp-2014/' rel='nofollow'>5th International Conference on Interactive Theorem Proving</a>, Vienna, Austria, July 14-17, 2014,
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 187 associated with FloC and the Vienna Summer of Logic.</td></tr>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 188
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 189 <tr><td >2013</td><td ><a class='urllink' href='http://itp2013.inria.fr' rel='nofollow'>4th International Conference on Interactive Theorem Proving</a>, Rennes, France, July 22-26, 2013</td></tr>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 190
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 191 <tr ><td >2012</td><td ><a class='urllink' href='http://itp2012.cs.princeton.edu' rel='nofollow'>3rd International Conference on Interactive Theorem Proving</a>, Princeton, NJ, US, August 13-15 2012</td></tr>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 192
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 193 <tr ><td >2011</td><td ><a class='urllink' href='http://itp2011.cs.ru.nl/ITP2011/Home.html' rel='nofollow'>2nd International Conference on Interactive Theorem Proving</a>, The Netherlands, August 22-25 2011</td></tr>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 194
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 195 <tr ><td >2010</td><td ><a class='urllink' href='http://www.floc-conference.org/ITP-home.html' rel='nofollow'>1st International Conference on Interactive Theorem Proving</a>, Edinburgh, Scotland, July 11-14, 2010</td></tr>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 196
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 197 <tr ><td >2009</td><td ><a class='urllink' href='http://isabelle.in.tum.de/nominal/activities/tphols09/' rel='nofollow'>The 22nd International Conference on Theorem Proving in Higher Order Logics</a>, Munich, Germany, August 17-20, 2009.</td></tr>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 198
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 199 <tr ><td >2008</td><td ><a class='urllink' href='http://users.encs.concordia.ca/%7Etphols08/TPHOLs2008/' rel='nofollow'>The 21th International Conference on Theorem Proving in Higher Order Logics</a>, Montreal, Canada, August 18-21, 2008.</td></tr>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 200
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 201 <tr ><td >2007</td><td ><a class='urllink' href='http://rsg.informatik.uni-kl.de/TPHOLs-2007/' rel='nofollow'>The 20th International Conference on Theorem Proving in Higher Order Logics</a>, Kaiserslautern, Germany, September 10-13, 2007.</td></tr>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 202
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 203 <tr ><td >2006</td><td >The 19th International Conference on Theorem Proving in Higher Order Logics merged with FloC, Seattle, August 17-20, 2006.</td></tr>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 204
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 205 <tr ><td >2005</td><td >The 18th International Conference on Theorem Proving in Higher Order Logics, Oxford, UK , 22-25 August 2005.</td></tr>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 206
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 207 <tr ><td >2004</td><td ><a class='urllink' href='http://www.cs.utah.edu/tphols2004' rel='nofollow'>The 17th International Conference on Theorem Proving in Higher Order Logics</a>, Park City, Utah, USA, 14-17 September 2004.</td></tr>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 208
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 209 <tr ><td >2003</td><td ><a class='urllink' href='http://tphols.informatik.uni-freiburg.de/' rel='nofollow'>The 16th International Conference on Theorem Proving in Higher Order Logics</a>, Rome, Italy, 9-12 September 2003.</td></tr>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 210
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 211 <tr ><td >2002</td><td >The 15th International Conference on Theorem Proving in Higher Order Logics, Hampton, Virginia, USA, 20-23 August 2002.</td></tr>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 212
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 213 <tr ><td >2001</td><td ><a class='urllink' href='http://www.dcs.gla.ac.uk/TPHOLs2001/' rel='nofollow'>The 14th International Conference on Theorem Proving in Higher Order Logics</a>, Edinburgh, Scotland, 3-6 September 2001.</td></tr>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 214 <tr ><td >2000</td><td >The 13th International Conference on Theorem Proving in Higher Order Logics, Portland, Oregon, USA, 14-18 August 2000.</td></tr>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 215
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 216 <tr ><td >1999</td><td >The 12th International Conference on Theorem Proving in Higher Order Logics, Unversity of Nice-Sophia-Antipolis, Nice, France, 14-17 September 1999.</td></tr>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 217
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 218 <tr ><td >1998</td><td ><a class='urllink' href='http://cs.anu.edu.au/TPHOLs98/' rel='nofollow'>The 11th International Conference on Theorem Proving in Higher Order Logics</a>, The Australian National University, Canberra, Australia, 28 September - 1 October 1998.</td></tr>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 219
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 220 <tr ><td >1997</td><td >The 10th International Conference on Theorem Proving in Higher Order Logics, Bell Labs, Murray Hill, New Jersey, USA, 19-22 August 1997.</td></tr>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 221
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 222 <tr ><td >1996</td><td >The 9th International Conference on Theorem Proving in Higher Order Logics, Turku Center for Computer Science and Åbo Akademi University, Turku, Finland, 26-30 August 1996.</td></tr>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 223
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 224 <tr ><td >1995</td><td >The 8th International Workshop on Higher Order Logic Theorem Proving and its Applications, Aspen Grove, Utah, USA, 11-14 September 1995.</td></tr>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 225
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 226 <tr ><td >1994</td><td >The 7th International Workshop on Higher Order Logic Theorem Proving and its Applications, Valletta, Malta, 19-22 September 1994.</td></tr>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 227
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 228 <tr ><td >1993</td><td >The 6th International Workshop on Higher Order Logic Theorem Proving and its Applications, Vancouver, B.C., Canada, 10-13 August 1993.</td></tr>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 229
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 230 <tr ><td >1992</td><td >The 5th International Workshop on Higher Order Logic Theorem Proving and its Applications, IMEC, Leuven, Belgium, 21-24 September 1992.</td></tr>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 231
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 232 <tr ><td >1991</td><td >The 4th International Workshop on the HOL Theorem Proving System and its Applications, Davis, California, USA, 28-30 August 1991.</td></tr>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 233
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 234 <tr ><td >1990</td><td >The 3rd International HOL Users Meeting, Aarhus University, Denmark, 1-2 October 1990.</td></tr>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 235
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 236 <tr ><td >1989</td><td >The 2nd International HOL Users Meeting, Trinity Hall, Cambridge, 14-15 December 1989.</td></tr>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 237
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 238 <tr ><td >1988</td><td >The 1st International HOL Users Meeting, Sidney Sussex College, Cambridge, 29-30 September 1988.</td></tr>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 239
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 240 </table>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 241
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 242 </TD>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 243 </TR>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 244 </TABLE>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 245
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 246 <hr>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 247 <a href="http://validator.w3.org/check/referer">[Validate this page.]</a>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 248 </body>
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
+ − 249 </html>