ITP 2021 2021 : International Conference on Interactive Theorem Proving

The International conference on Interactive Theorem Proving

(ITP 2021) will take place on June 29-July 1, 2021 in Rome,

Italy. It will be co-located with LICS and ICTCS

conferences.

ITP will carefully monitor the development of the COVID-19

pandemic, and take guidance from the health authorities, to

determine whether ITP21 will be held physically, virtually

or in a hybrid manner.

The ITP conference series is concerned with all aspects of

interactive theorem proving, ranging from theoretical

foundations to implementation aspects and applications in

program verification, security, and the formalization of

mathematics. This will be the 12th conference in the ITP

series, while predecessor conferences from which it has

evolved have been going since 1988.

Paper Submission

================

ITP welcomes submissions describing original research on

all aspects of interactive theorem proving and its

applications. Suggested topics include, but are not limited

to, the following:

* formalizations of computational models

* improvements in theorem prover technology

* formalizations of mathematics

* integration with automated provers and other symbolic tools

* verification of security algorithms

* industrial applications of interactive theorem provers

* formal aspects of hardware and software

* user interfaces for interactive theorem provers

* use of theorem provers in education

* concise and elegant worked examples of formalizations (proof pearls)

Submissions will undergo single-blind peer review. They

should be no more than 16 pages in length excluding

bibliographic references and are to be submitted in PDF

format via EasyChair via the following link:

https://easychair.org/conferences/?conf=itp2021

We also welcome short papers, which can be used to describe

interesting work that is still ongoing and not fully

mature. Such a preliminary report is limited to 6 pages and

may consist of an extended abstract. Each of these papers

should bear the phrase “(short paper)” beneath the

title. Accepted submissions in this category will be

published in the main proceedings and will be presented as

short talks.

All submissions are expected to be accompanied by

verifiable evidence of a suitable implementation, such as

the source files of a formalization for the proof assistant

used.

Important Dates

===============

* Abstract submission deadline: January 25, 2021

* Paper submission deadline: February 1, 2021

* Author notification: March 25, 2021

* Camera-ready copy due: April 20, 2021

* Conference: June 29-July 1, 2021

Publication Details

===================

The conference proceedings will be published in the LIPIcs

series (“Leibniz International Proceedings in

Informatics”). This was chosen in large part because of its

commitment to free and open access to all papers. For more

information on the series see

https://www.dagstuhl.de/en/publications/lipics and for more

detailed instructions for authors on document preparation:

https://www.dagstuhl.de/en/publications/lipics/instructions-for-authors/