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. _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
