112 <h3>The TPHOLs conference series</h3>

   113 

   114 <p>TPHOLs 2009 was the twenty-second in a series of international

   115 conferences on the applications of higher order logic theorem proving.

   116 The first three (two at Cambridge and one at Århus) were informal

   117 users' meetings for the HOL system and were the only ones without

   118 published papers. Between 1991 and 1995 (Davis, Leuven, Vancouver,

   119 Malta, Utah) the conference entertained an increasingly wide field of

   120 interest.  </p>

   121 

   122 <p>The evolution resulted in the program committee for the meeting in

   123 Turku (1996) deeming that the scope of the conference included all

   124 reasoning tools for higher order logics and adopted the name TPHOLs,

   125 being an acronym for Theorem Proving in Higher Order Logics. (The

   126 final letter being considered necessary to break the direct connection

   127 between the conference and the HOL system.) This decision was strongly

   128 endorsed at the business sessions at Turku and Murray Hill (1997).

   129 </p>

   130 

   131 <p>An extensive collection of links to various aspects of previous

   132 conferences in the series may be found below.  </p>

   133 

   134 <h3>Associated communities</h3>

   135 <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>

   136 

   137 <a class='urllink' href='http://abella.cs.umn.edu' rel='nofollow'>Abella</a>  - 

   138 <a class='urllink' href='http://wiki.portal.chalmers.se/agda/pmwiki.php' rel='nofollow'>Agda</a>  -  

   139 <a class='urllink' href='http://www.cs.utexas.edu/users/moore/acl2' rel='nofollow'>ACL2</a> -  

   140 <a class='urllink' href='http://coq.inria.fr' rel='nofollow'>Coq</a> -  

   141 <a class='urllink' href='http://www.cl.cam.ac.uk/research/hvg/HOL' rel='nofollow'>HOL</a> -  

   142 <a class='urllink' href='http://imps.mcmaster.ca' rel='nofollow'>IMPS</a> -

   143 <a class='urllink' href='http://www.cl.cam.ac.uk/research/hvg/Isabelle' rel='nofollow'>Isabelle</a> -

   144 <a class='urllink' href='http://www.dcs.ed.ac.uk/home/lego' rel='nofollow'>LEGO</a> -

   145 <a class='urllink' href='http://matita.cs.unibo.it' rel='nofollow'>Matita</a> -

   146 <a class='urllink' href='http://www.nuprl.org' rel='nofollow'>Nuprl</a> -

   147 <a class='urllink' href='http://www.lemma-one.com/ProofPower/index/index.html' rel='nofollow'>ProofPower</a> -

   148 <a class='urllink' href='http://pvs.csl.sri.com' rel='nofollow'>PVS</a> - 

   149 </p>

   150 

   151 <h3>Traditions</h3>

   152 

   153 <p>A longstanding convention is that the annual conference should be

   154 held in a continent different to the location of the previous meeting.

   155 Another tradition is that the organizers for each meeting handle all

   156 aspects of the conference for the whole year in consultation with the

   157 previous few organizers. This includes selection of the programme

   158 committee, editing the proceedings, fund-raising, programme and local

   159 arrangements. Another responsibility of the organizers in year n is to

   160 call for bids and conduct a poll for the selection of the venue for

   161 the conference in year n+1.  </p>

   162 

   163 <h3>ITP and TPHOLs conferences</h3>

   164 

   165 <table border='1'>

   166 <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,

   167 associated with FloC and the Vienna Summer of Logic.</td></tr>

   168   

   169 <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>

   170 

   171 <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>

   172 

   173 <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>

   174 

   175 <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>

   176 

   177 <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>

   178 

   179 <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>

   180 

   181 <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>

   182 

   183 <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>

   184 

   185 <tr ><td >2005</td><td >The 18th International Conference on Theorem Proving in Higher Order Logics, Oxford, UK , 22-25 August 2005.</td></tr>

   186 

   187 <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>

   188 

   189 <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>

   190 

   191 <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>

   192 

   193 <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>

   194 <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>

   195 

   196 <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>

   197 

   198 <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>

   199 

   200 <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>

   201 

   202 <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>

   203 

   204 <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>

   205 

   206 <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>

   207 

   208 <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>

   209 

   210 <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>

   211 

   212 <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>

   213 

   214 <tr ><td >1990</td><td >The 3rd International HOL Users Meeting, Aarhus University, Denmark, 1-2 October 1990.</td></tr>

   215 

   216 <tr ><td >1989</td><td >The 2nd International HOL Users Meeting, Trinity Hall, Cambridge, 14-15 December 1989.</td></tr>

   217 

   218 <tr ><td >1988</td><td >The 1st International HOL Users Meeting, Sidney Sussex College, Cambridge, 29-30 September 1988.</td></tr>

   219 

   220 </table>