Interactive Theorem Proving (ITP) is an annual international

academic conference An academic conference or scientific conference (also congress, symposium, workshop, or meeting) is an event for researchers (not necessarily academics) to present and discuss their scholarly work. Together with academic or scientific journals an ...

on the topic of

automated theorem proving Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a maj ...

proof assistant In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor ...

s and related topics, ranging from theoretical foundations to implementation aspects and applications in

program verification In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal metho ...

security Security is protection from, or resilience against, potential harm (or other unwanted coercive change) caused by others, by restraining the freedom of others to act. Beneficiaries (technically referents) of security may be of persons and social ...

, and formalization of mathematics. ITP brings together the communities using many systems based on higher-order logic such as

ACL2 ACL2 ("A Computational Logic for Applicative Common Lisp") is a software system consisting of a programming language, created by Timothy Still it was an extensible theory in a first-order logic, and an automated theorem prover. ACL2 is designed to ...

Coq Coq is an interactive theorem prover first released in 1989. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proof ...

Mizar Mizar is a second-magnitude star in the handle of the Big Dipper asterism in the constellation of Ursa Major. It has the Bayer designation ζ Ursae Majoris ( Latinised as Zeta Ursae Majoris). It forms a well-known naked eye d ...

, HOL,

Isabelle Isabel is a female name of Spanish origin. Isabelle is a name that is similar, but it is of French origin. It originates as the medieval Spanish form of '' Elisabeth'' (ultimately Hebrew ''Elisheva''), Arising in the 12th century, it became popul ...

Lean Lean, leaning or LEAN may refer to: Business practices * Lean thinking, a business methodology adopted in various fields ** Lean construction, an adaption of lean manufacturing principles to the design and construction process ** Lean governm ...

, NuPRL, PVS, and

Twelf Twelf is an implementation of the logical framework LF developed by Frank Pfenning and Carsten Schürmann at Carnegie Mellon University. It is used for logic programming and for the formalization of programming language theory. Introduction At i ...

. Individual workshops or meetings devoted to individual systems are usually held concurrently with the conference. Together with CADE and

TABLEAUX The International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX) is an annual international academic conference that deals with all aspects of automated reasoning with analytic tableaux. Periodically, it joi ...

, ITP is usually one of the three main conferences of the

International Joint Conference on Automated Reasoning The International Joint Conference on Automated Reasoning (IJCAR) is a series of conferences on the topics of automated reasoning, automated deduction, and related fields. It is organized semi-regularly as a merger of other meetings. IJCAR replace ...

(IJCAR) whenever it convenes,

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 Springer or springers may refer to: Publishers * Springer Science+Business Media, aka Springer International Publishing, a worldwide publishing group founded in 1842 in Germany formerly known as Springer-Verlag. ** Springer Nature, a multinationa ...

Lecture Notes in Computer Science ''Lecture Notes in Computer Science'' is a series of computer science books published by Springer Science+Business Media since 1973. Overview The series contains proceedings, post-proceedings, monographs, and Festschrifts. In addition, tutorials, ...

series. It has also entertained an increasingly wide field of interest.

External links

* Automated theorem proving Theoretical computer science conferences Logic conferences {{Compu-conference-stub