<div dir="ltr"><div>                             SECOND CALL FOR PAPERS</div><div><br></div><div>                                    ITP 2018</div><div>          9th International Conference on Interactive Theorem Proving</div><div>                                   Oxford, UK</div><div>                                 July 9-12, 2018</div><div>                            <a href="https://itp2018.inria.fr/">https://itp2018.inria.fr/</a></div><div><br></div><div><br></div><div>Submission Deadlines: Thursday,  January 25, 2018 (abstracts)</div><div>                      Wednesday, January 31, 2018 (full papers)</div><div><br></div><div>GENERAL INFORMATION</div><div>The ITP conference series is concerned with all topics related to interactive</div><div>theorem proving, ranging from theoretical foundations to implementation aspects</div><div>and applications in program verification, security, and formalization of</div><div>mathematics. ITP is the evolution of the TPHOLs conference series to the broad</div><div>field of interactive theorem proving. TPHOLs meetings took place every year from</div><div>1988 until 2009. The ninth ITP conference, ITP 2018, will be held in Oxford,</div><div>July 9-12, 2018.</div><div><br></div><div>SCOPE OF CONFERENCE</div><div>ITP welcomes submissions describing original research on all aspects of</div><div>interactive theorem proving and its applications. Suggested topics include but</div><div>are not limited to the following:</div><div><br></div><div>*  formal aspects of hardware and software</div><div>*  formalizations of mathematics</div><div>*  improvements in theorem prover technology</div><div>*  user interfaces for interactive theorem provers</div><div>*  formalizations of computational models</div><div>*  verification of security algorithms</div><div>*  use of theorem provers in education</div><div>*  industrial applications of interactive theorem provers</div><div>*  concise and elegant worked examples of formalizations (proof pearls)</div><div><br></div><div>PUBLICATION DETAILS</div><div>The proceedings of the symposium will be published in the Springer's LNCS</div><div>series. The organizers intend to publish expanded versions of a select subset of</div><div>papers from the conference in a special issue of the Journal of Automated Reasoning.</div><div><br></div><div>PAPER SUBMISSIONS</div><div>All submissions must be original, unpublished, and not submitted concurrently</div><div>for publication elsewhere. Furthermore, when appropriate, submissions are</div><div>expected to be accompanied by verifiable evidence of a suitable implementation,</div><div>such as the source files of a formalization for the proof assistant used. These</div><div>materials can be uploaded with the submission, or made available on the web. In</div><div>either case, the submission should provide clear instructions to referees as to</div><div>how to obtain the relevant materials and compile them or check them, as the case</div><div>may be.</div><div><br></div><div>Submissions will be subjected to single-blind peer review. They should be no</div><div>more than 16 pages in length excluding bibliographic references and are to be</div><div>submitted in PDF via EasyChair at the following address:</div><div><br></div><div>  <a href="https://easychair.org/conferences/?conf=itp2018">https://easychair.org/conferences/?conf=itp2018</a></div><div><br></div><div>Submissions must conform to the LNCS style in LaTeX. An author of each accepted</div><div>paper is expected to present it at the conference and will be required to sign a</div><div>copyright release form.</div><div><br></div><div>In addition to regular papers, described above, there will be a section for</div><div>shorter papers, which can be used to describe interesting work that is still</div><div>ongoing and not fully mature. Such a preliminary report is limited to 6 pages</div><div>and may consist of an extended abstract. Each of these papers should bear the</div><div>phrase "(short paper)" beneath the title, and will be refereed and be expected</div><div>to present innovative and promising ideas, possibly in early form. Accepted</div><div>submissions in this category will be published in the main proceedings and will</div><div>be presented as short talks.</div><div><br></div><div>IMPORTANT DATES</div><div>Abstract submission deadline: January 25, 2018</div><div>Full paper submission deadline: January 31, 2018</div><div>Author notification: March 31, 2018</div><div>Camera-ready papers: May 25, 2018</div><div>Conference: July 9-12, 2018</div><div><br></div><div>PROGRAM COMMITTEE</div><div>Jeremy Avigad, Carnegie Mellon University (chair)</div><div>Assia Mahboubi, Inria (chair)</div><div>Andreas Abel, Gothenburg University</div><div>Benedikt Ahrens, University of Birmingham</div><div>June Andronick, CSIRO|Data61 and UNSW</div><div>Adam Chlipala, Massachusetts Institute of Technology</div><div>Jasmin Christian Blanchette, Vrije Universiteit Amsterdam</div><div>Thierry Coquand, Chalmers University of Technology</div><div>Karl Crary, Carnegie Mellon University</div><div>Delphine Demange, IRISA / University of Rennes 1</div><div>Timothy Griffin, University of Cambridge</div><div>Thomas Hales, University of Pittsburgh</div><div>John Harrison, Intel</div><div>Johannes Hölzl, Vrije Universiteit Amsterdam</div><div>Chung-Kil Hur, Seoul National University</div><div>Jacques-Henri Jourdan, LRI, CNRS, Université Paris-Sud</div><div>Cezary Kaliszyk, University of Innsbruck</div><div>Ambrus Kaposi, Eötvös Loránd University, Budapest</div><div>Chantal Keller, LRI, CNRS, Université Paris-Sud</div><div>Panagiotis Manolios, Northeastern University</div><div>Mariano Moscato, National Institute of Aerospace</div><div>Leonardo de Moura, Microsoft Research</div><div>Magnus O. Myreen, Chalmers University of Technology</div><div>Tobias Nipkow, Technische Universität München</div><div>Lawrence Paulson, University of Cambridge</div><div>André Platzer, Carnegie Mellon University</div><div>Andrei Popescu, Middlesex University London</div><div>Matthieu Sozeau, Inria</div><div>Pierre-Yves Strub, École Polytechnique</div><div>Enrico Tassi, Inria</div><div>Zachary Tatlock, University of Washington</div><div>Laurent Théry, Inria</div><div>Cesare Tinelli, The University of Iowa</div><div>Alwen Tiu, Australian National University</div><div>Makarius Wenzel, <a href="http://sketis.net">sketis.net</a></div><div>Freek Wiedijk, Radboud University Nijmegen</div><div><br></div><div>CONTACT INFORMATION</div><div>Jeremy Avigad</div><div>Assia Mahboubi</div><div><a href="mailto:itp2018@easychair.org">itp2018@easychair.org</a></div><div><a href="https://itp2018.inria.fr/">https://itp2018.inria.fr/</a></div></div>