History

ITP 2016 is the seventh conference on Interactive Theorem Proving and related topics, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and formalization of mathematics. The inaugural meeting of ITP was held on 11 to 14 July 2010 in Edinburgh, Scotland, as part of the Federated Logic Conference (FLoC, 9 to 21 July 2010). ITP is the evolution of the TPHOLs conference series to the broad field of interactive theorem proving. TPHOLs meetings took place every year from 1988 until 2009.

The TPHOLs Conference Series

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, an acronym for Theorem Proving in Higher Order Logics. (The final letter was 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.

Associated Communities

An inspection of the proceedings of recent conferences show that the conference accommodates the user communities of a number of interactive theorem proving systems. The interested reader is referred to the web sites for the following provers:

Abella ⋅ ACL2 ⋅ Agda ⋅ Beluga ⋅ Coq ⋅ HOL ⋅ IMPS ⋅ Isabelle ⋅ Lean ⋅ LEGO ⋅ Matita ⋅ Mizar ⋅ Nuprl ⋅ ProofPower ⋅ PVS ⋅ TLA+ Proof System

Traditions

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, program, 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.

Past ITP and TPHOLs Conferences

2015 6th International Conference on Interactive Theorem Proving, Nanjing, China, August 24–27, 2015
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

Comments are closed.