Interactive Theorem Proving (ITP) is an annual international academic conference on the topic of automated theorem proving, proof assistants and related topics, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and formalization of mathematics.
ITP brings together the communities using many systems based on higher-order logic such as ACL2, Coq, Mizar, HOL, Isabelle, Lean, NuPRL, PVS, and Twelf.
Together with CADE and TABLEAUX, ITP is usually one of the three main conferences of the International Joint Conference on Automated Reasoning (IJCAR) whenever it convenes, The inaugural meeting of ITP was held on 11–14 July 2010 in Edinburgh, Scotland, as part of the Federated Logic Conference.
It is the extension of the Theorem Proving in Higher Order Logics (TPHOLs) conference series to the broad field of interactive theorem proving.
The first three were informal users' meetings for the HOL system and were the only ones without published papers.