[Agda] ITP 2025: Second Call for Papers

[Tom de Jong]

16th International Conference on Interactive Theorem Proving - ITP'25

Reykjavik, Iceland, 27 September-3 October 2025

https://icetcs.github.io/frocos-itp-tableaux25/itp/

Second call for papers

# Background

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 16th conference in the
ITP series, while predecessor conferences from which it has evolved have
been going since 1988.

# Important dates

-   Abstract submission deadline: March 12, 2025
-   Paper submission deadline: March 19, 2025
-   Author notification: May 23, 2025
-   Camera-ready copy due: June 27, 2025

# Topics

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 interactive 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 specification and verification 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)

# Paper categories and submission

We welcome regular papers and short papers. Submission for both is
lightweight double-blind. This means that (1) author names and
institutions must be omitted using the the anonymous option of the
document class, (2) references to authors' own related work should be in
the third person, and (3) the identity of authors will be reveiled to
reviewers once they have submitted a first draft of their review.

The purpose of this process is to help the PC and external reviewers
come to an initial judgment about the paper without bias, not to make it
impossible for them to discover the authors if they were to try. Nothing
should be done in the name of anonymity that weakens the submission or
makes the job of reviewing it more difficult. In particular, important
background references should not be omitted or anonymized. In addition,
authors are free to disseminate their ideas or draft versions of their
papers as usual. For example, authors may post drafts of their papers on
the web or give talks on their research ideas.

Regular papers must:

-   be no more than 16 pages in length excluding bibliographic
    references
-   not include an appendix, and
-   be in LIPIcs format.

 Short papers can be used to describe interesting work that is still
ongoing and not fully mature. Accepted short papers will be published in
the main proceedings and will be presented as short talks. Short papers must

 -  be no more than 6 pages in length excluding bibliographic references
and may consist of an extended abstract,
 -  have the phrase "Short paper" as a subtitle,
 -  not include an appendix, and
 -  be in LIPIcs format.

Both categories of papers must be prepared in LaTeX using the
lipics-v2021 style (v2021.1.3) and must be submitted electronically as
pdf files through HotCRP:

https://itp25.hotcrp.com

All submissions are expected to be accompanied by supplementary material
containing verifiable evidence of a suitable implementation, such as the
source files of a formalization for the proof assistant used. They also
need to have a README explaining how the source files can be compiled
and what exact version of the proof assistant and packages to use.

Two forms of supplementary material may be submitted: (1) Anonymous
supplementary material is made available to the reviewers before they
submit their first-draft reviews. (2) Non-anonymous supplementary
material is made available to the reviewers after they have submitted
their first-draft reviews and have learned the identity of the authors.
We strongly encourage anonymous supplementary material whenever possible.

# Publication

The conference proceedings will be published in Dagstuhl Publishing\'s
[Leibniz International Proceedings in Informatics
(LIPIcs)](https://drops.dagstuhl.de/entities/series/LIPIcs) series in
Gold Open Access under the [CC-BY-4.0
license](https://creativecommons.org/licenses/by/4.0/).

# Registration and Participation

Remote attendance of the conference will be possible for a low or no
fee. For all accepted papers, at least one author must pay a full
registration fee. For presenters we strongly encourage physical
participation since coming to the conference benefits the dissemination
of the paper and the overall quality of the conference. Remote talks are
only possible if agreed with the organizers by the registration
deadline, but still one author must pay the full registration fee.

# Program committee

    Yannick Forster (co-chair), Inria Paris
    Chantal Keller (co-chair), LMF, Université Paris-Saclay
    Mohammad Abdulaziz, King's College London
    Reynald Affeldt, AIST
    Jeremy Avigad, Carnegie Mellon University
    Anne Baanen, Vrije Universiteit Amsterdam, Lean FRO LLC
    Małgorzata Biernacka, University of Wroclaw
    Mario Carneiro, Chalmers University of Technology
    Évelyne Contejean, CNRS
    María Inés de Frutos Fernández, University of Bonn
    Tom de Jong, University of Nottingham
    Thaynara Arielly de Lima, Universidade Federal de Goiás
    Manuel Eberl, University of Innsbruck
    Chelsea Edmonds, University of Sheffield
    Andres Erbsen, Google
    Thiago Felicissimo, Inria Rennes
    Amy Felty, University of Ottawa
    Asta Halkjær From, University of Copenhagen
    Aymeric Fromherz, Inria Paris
    Ruben Gamboa, University of Wyoming
    Hrutvik Kanabar, Arm
    Dominik Kirst, Inria
    Angeliki Koutsoukou-Argyraki, University of Cambridge
    Vincent Laporte, Inria Nancy
    Meven Lennon-Bertrand, University of Cambridge
    Robert Lewis, Brown University
    Heather Macbeth, Fordham University, NYC
    Paolo Masci, NASA
    Cody Roux, AWS
    Yong Kiam Tan, Institute for Infocomm Research, A*STAR, Singapore
    Andrew Tolmach, Portland State University
    Sophie Tourret, Inria Nancy
    Dmitriy Traytel, University of Copenhagen
    Niccolò Veltri, Tallinn University of Technology
    Bohua Zhan, Huawei Technologies Co., Ltd.