The Next ITP Conference

ITP 2025 is the fifteenth conference on Interactive Theorem Proving. It will take place in Reykjavik, Iceland, September 27-October 3, 2025, co-located with FroCoS and TABLEAUX.

...

Past ITP and TPHOLs Conferences

2024
Tbilisi, Georgia
September 9–14, 2024
2023
Bialystok, Poland
July 31 – August 4, 2023
2022
Haifa, Israel
July 31 – August 12, 2022
associated with FLoC, the Federated Logic Conference
2020
Paris, France
29 June – 5 July 2020
merged with IJCAR
2019
Portland, OR, USA
September 8-13 2019
2017
8th International Conference on Interactive Theorem Proving
Brasília, Brazil
September 26-29, 2017
2016
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
2012
3rd International Conference on Interactive Theorem Proving
Princeton, NJ, US
August 13–15 2012
2011
2010
1st International Conference on Interactive Theorem Proving
Edinburgh, Scotland
July 11–14, 2010
associated with FLoC
2007
The 20th International Conference on Theorem Proving in Higher Order Logics
Kaiserslautern, Germany
September 10–13, 2007
2004
2002
1999
The 12th International Conference on Theorem Proving in Higher Order Logics
University 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
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

Associated Communities

An inspection of the proceedings of recent conferences shows 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:

AbellaACL2AgdaArendBelugaCoqHOLIMPSIsabelleLeanLEGOMatitaMizarNuprlProofPowerPVSTLA+ Proof System

History

The ITP conference series is dedicated to 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 adopting 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).

Traditions

A long-standing 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 program 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.

Statistics