[Hol-info] ITP 2026: Call for Papers

[Slusarz, N. <nd...@hw...>]

ITP 2026: Call for Papers
------------------------------------------------
https://itp-conference-2026.github.io/

The International Conference on Interactive Theorem Proving (ITP 2026)
will take place on 26-29 July, 2026 in Lisbon, Portugal.
It will be part of FLoC 2026. ITP 2026 is part of the ITP conference series
whose history goes back to 1988.

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

##Important Dates

Abstract Deadline: February 12, 2026 (AOE)
Paper Submission Deadline: February 19, 2026 (AOE)
Author Notification: April 26, 2026
Camera-ready Copy: May 24, 2026
Conference: July 26-29, 2026

##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 and neurosymbolic tools
- 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)
- sound methods for using AI in proof discovery


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 anonymous option of the document
class, (2) references to authors' own related work should be in the third
person.

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):

https://submission.dagstuhl.de/series/details/LIPIcs#author

and must be submitted electronically as pdf files through
HotCRP. All submissions are expected to be accompanied by anonymised
supplementary material containing verifiable evidence of a suitable
implementation, such as the source files of a formalization for the
proof assistant used.

##Publication

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.

##Registration, Participation and Colocated Workshops

Refer to FLoC 2026 webpage: https://www.floc26.org/

## Program Co-chairs

Ekaterina Komendantskaya, University of Southampton, Heriot-Watt University
Tobias Nipkow, Technical University of Munich

##Publicity Chair

Natalia Ślusarz, Heriot-Watt University

##Programme Committee

Mohammad Abdulaziz, King's College London
Reynald Affeldt, AIST
Guillaume Allais, University of Strathclyde
Robert Atkey, University of Strathclyde
Jeremy Avigad, Carnegie Mellon University
Jasmin Blanchette, LMU Munich
Sandrine Blazy, University of Rennes
Sylvie Boldo, INRIA
Edwin Brady,  University of St Andrews
Alessandro Bruni, ITU Copenhagen
Swarat Chaudhuri, University of Texas, Austin
Matthew Daggitt,  The University of Western Australia
Sander Dahmen, VU Amsterdam
Floris van Doorn,  University of Bonn
Manuel Eberl, University of Innsbruck
Amy Felty, University of Ottawa
Jacques Fleuriot, University of Edinburgh
Yannick Forster, INRIA
María Inés de Frutos-Fernández, University of Bonn
Ralf Jung, ETH Zürich
Ambrus Kaposi, Eötvös Loránd University
Yonghyun Kim,  MPI-SP
Katherine Kosaian, University of Iowa
K. Rustan M. Leino, Amazon Web Services
Robert Y. Lewis, Brown University
Heather Macbeth, Imperial College London
Assia Mahboubi, INRIA
William Mansky, University of Illinois Chicago
Micaela Mayero, Sorbonne Paris Nord University
Magnus Myreen, Chalmers University of Technology
Grant Passmore, Imandra
Andrei Popescu, University of Sheffield
François Pottier, INRIA
Talia Ringer,  University of Illinois at Urbana-Champaign
Christine Rizkallah, The University of Melbourne
Nikhil Swamy,  Microsoft Redmond
Nicolas Tabareau,  INRIA
Yong Kiam Tan, Nanyang Technological University and Institute for Infocomm
               Research, A*STAR, Singapore
Joseph Tassarotti, New York University
Enrico Tassi, INRIA
Laura Titolo, Code Metal
Dmitriy Traytel, University of Copenhagen
Niccolò Veltri, Tallinn University of Technology
Akihisa Yamada, AIST
________________________________

Founded in 1821, Heriot-Watt is a leader in ideas and solutions. With campuses and students across the entire globe we span the world, delivering innovation and educational excellence in business, engineering, design and the physical, social and life sciences. This email is generated from the Heriot-Watt University Group, which includes:

  1.  Heriot-Watt University, a Scottish charity registered under number SC000278
  2.  Heriot- Watt Services Limited (Oriam), Scotland's national performance centre for sport. Heriot-Watt Services Limited is a private limited company registered is Scotland with registered number SC271030 and registered office at Research & Enterprise Services Heriot-Watt University, Riccarton, Edinburgh, EH14 4AS.

The contents (including any attachments) are confidential. If you are not the intended recipient of this e-mail, any disclosure, copying, distribution or use of its contents is strictly prohibited, and you should please notify the sender immediately and then delete it (including any attachments) from your system.