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