TPHOLs 2009 was the twenty-second in a series of international -conferences on the applications of higher order logic theorem proving. -The first three (two at Cambridge and one at Århus) were informal -users' meetings for the HOL system and were the only ones without -published papers. Between 1991 and 1995 (Davis, Leuven, Vancouver, -Malta, Utah) the conference entertained an increasingly wide field of -interest.
- -The evolution resulted in the program committee for the meeting in -Turku (1996) deeming that the scope of the conference included all -reasoning tools for higher order logics and adopted the name TPHOLs, -being an acronym for Theorem Proving in Higher Order Logics. (The -final letter being considered necessary to break the direct connection -between the conference and the HOL system.) This decision was strongly -endorsed at the business sessions at Turku and Murray Hill (1997). -
- -An extensive collection of links to various aspects of previous -conferences in the series may be found below.
- -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:
-
-Abella -
-Agda -
-ACL2 -
-Coq -
-HOL -
-IMPS -
-Isabelle -
-LEGO -
-Matita -
-Nuprl -
-ProofPower -
-PVS -
-
A longstanding convention is that the annual conference should be -held in a continent different to the location of the previous meeting. -Another tradition is that the organizers for each meeting handle all -aspects of the conference for the whole year in consultation with the -previous few organizers. This includes selection of the programme -committee, editing the proceedings, fund-raising, programme and local -arrangements. Another responsibility of the organizers in year n is to -call for bids and conduct a poll for the selection of the venue for -the conference in year n+1.
- -| 2014 | 5th International Conference on Interactive Theorem Proving, Vienna, Austria, July 14-17, 2014, -associated with FloC and the Vienna Summer of Logic. |
| 2013 | 4th International Conference on Interactive Theorem Proving, Rennes, France, July 22-26, 2013 |
| 2012 | 3rd International Conference on Interactive Theorem Proving, Princeton, NJ, US, August 13-15 2012 |
| 2011 | 2nd International Conference on Interactive Theorem Proving, The Netherlands, August 22-25 2011 |
| 2010 | 1st International Conference on Interactive Theorem Proving, Edinburgh, Scotland, July 11-14, 2010 |
| 2009 | The 22nd International Conference on Theorem Proving in Higher Order Logics, Munich, Germany, August 17-20, 2009. |
| 2008 | The 21th International Conference on Theorem Proving in Higher Order Logics, Montreal, Canada, August 18-21, 2008. |
| 2007 | The 20th International Conference on Theorem Proving in Higher Order Logics, Kaiserslautern, Germany, September 10-13, 2007. |
| 2006 | The 19th International Conference on Theorem Proving in Higher Order Logics merged with FloC, Seattle, August 17-20, 2006. |
| 2005 | The 18th International Conference on Theorem Proving in Higher Order Logics, Oxford, UK , 22-25 August 2005. |
| 2004 | The 17th International Conference on Theorem Proving in Higher Order Logics, Park City, Utah, USA, 14-17 September 2004. |
| 2003 | The 16th International Conference on Theorem Proving in Higher Order Logics, Rome, Italy, 9-12 September 2003. |
| 2002 | The 15th International Conference on Theorem Proving in Higher Order Logics, Hampton, Virginia, USA, 20-23 August 2002. |
| 2001 | The 14th International Conference on Theorem Proving in Higher Order Logics, Edinburgh, Scotland, 3-6 September 2001. |
| 2000 | The 13th International Conference on Theorem Proving in Higher Order Logics, Portland, Oregon, USA, 14-18 August 2000. |
| 1999 | The 12th International Conference on Theorem Proving in Higher Order Logics, Unversity of Nice-Sophia-Antipolis, Nice, France, 14-17 September 1999. |
| 1998 | The 11th International Conference on Theorem Proving in Higher Order Logics, The Australian National University, Canberra, Australia, 28 September - 1 October 1998. |
| 1997 | The 10th International Conference on Theorem Proving in Higher Order Logics, Bell Labs, Murray Hill, New Jersey, USA, 19-22 August 1997. |
| 1996 | 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. |
| 1995 | The 8th International Workshop on Higher Order Logic Theorem Proving and its Applications, Aspen Grove, Utah, USA, 11-14 September 1995. |
| 1994 | The 7th International Workshop on Higher Order Logic Theorem Proving and its Applications, Valletta, Malta, 19-22 September 1994. |
| 1993 | The 6th International Workshop on Higher Order Logic Theorem Proving and its Applications, Vancouver, B.C., Canada, 10-13 August 1993. |
| 1992 | The 5th International Workshop on Higher Order Logic Theorem Proving and its Applications, IMEC, Leuven, Belgium, 21-24 September 1992. |
| 1991 | The 4th International Workshop on the HOL Theorem Proving System and its Applications, Davis, California, USA, 28-30 August 1991. |
| 1990 | The 3rd International HOL Users Meeting, Aarhus University, Denmark, 1-2 October 1990. |
| 1989 | The 2nd International HOL Users Meeting, Trinity Hall, Cambridge, 14-15 December 1989. |
| 1988 | The 1st International HOL Users Meeting, Sidney Sussex College, Cambridge, 29-30 September 1988. |