Email Gateway (Jan 25 2025 at 15:36): Email Gateway (Jan 25 2025 at 15:36):From: Yannick Forster <yannick.forster@inria.fr>
16th International Conference on Interactive Theorem Proving - ITP'25
Reykjavik, Iceland, 27 September-3 October 2025
https://icetcs.github.io/frocos-itp-tableaux25/itp/
First call for papers
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.
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:
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,
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:
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.
The conference proceedings will be published in Dagstuhl Publishing\'s
Leibniz International Proceedings in Informatics
(LIPIcs) series in
Gold Open Access under the CC-BY-4.0
license.
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.
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, Institute of Software, Chinese Academy of Sciences
Last updated: Jan 30 2025 at 04:21 UTC