Top Qs
Timeline
Chat
Perspective
Interactive Theorem Proving (conference)
From Wikipedia, the free encyclopedia
Remove ads
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.
It is proposed that this article be deleted because of the following concern:
If you can address this concern by improving, copyediting, sourcing, renaming, or merging the page, please edit this page and do so. You may remove this message if you improve the article or otherwise object to deletion for any reason. Although not required, you are encouraged to explain why you object to the deletion, either in your edit summary or on the talk page. If this template is removed, do not replace it. The article may be deleted if this message remains in place for seven days, i.e., after 22:44, 10 December 2025 (UTC). Find sources: "Interactive Theorem Proving" conference – news · newspapers · books · scholar · JSTOR Nominator: Please consider notifying the author/project: {{subst:proposed deletion notify|Interactive Theorem Proving (conference)|concern=Unreferenced for 13 years. Fails GNG.}} ~~~~ |
 | This article may rely excessively on sources too closely associated with the subject, potentially preventing the article from being verifiable and neutral. (January 2025) |
ITP brings together the communities using many systems based on higher-order logic such as ACL2, Rocq, Mizar, HOL, Isabelle, Lean, NuPRL, PVS, and Twelf. Individual workshops or meetings devoted to individual systems are usually held concurrently with the conference.
Remove ads
History
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. TPHOLs meetings took place every year from 1988 until 2009.
The first three were informal users' meetings for the HOL system and were the only ones without published papers. Since 1990 TPHOLs has published formal peer-reviewed proceedings, published by Springer's Lecture Notes in Computer Science series. It has also entertained an increasingly wide field of interest.
Remove ads
External links
Wikiwand - on
Seamless Wikipedia browsing. On steroids.
Remove ads