The International Conference on Interactive Theorem Proving (ITP) is a premier venue for publishing research in the area of logical frameworks and interactive proof assistants. Its topics include both theoretical foundations and implementation aspects of the technology, as well as applications to verifying hardware and software systems to ensure their safety and security, and applications to the formal verification of mathematical results.

ITP grew out of TPHOLs conferences and ACL2 workshops that begin in the early 1990s. Previous editions of ITP have taken place in Brasília (Brazil), Nancy (France), Nanjing (China), Vienna (Austria), Rennes (France), Princeton (USA), Berg en Dal (The Netherlands) and Edinburgh (UK).

This ninth edition, ITP 2018, was part of the Federated Logic Conference (FLoC) 2018, and took place in Oxford, UK, from July 9 to July 12, 2018. We thank the FLoC organizing committee for undertaking the Herculean task of planning and organizing the event.

In all, 55 regular papers and 10 short papers were submitted to the conference. Each paper was reviewed by at least three people, either members of the program committee or external reviewers. The committee ultimately accepted 32 regular papers and 5 short papers.

ITP 2018 included memorial lectures in honor of Mike Gordon and Vladimir Voevodsky, two influential figures in interactive theorem proving who had passed way over the course of the previous year. John Harrison was invited to present the lecture for Gordon, and Daniel Grayson was invited to present the lecture for Voevodsky. In addition, Jean-Christophe Filliâtre was invited to present a third keynote talk.

The present volume collects all the scientific contributions to the conference as well as abstracts of the three keynote presentations. We are grateful to the members of the ITP steering committee for their guidance and advice, and especially grateful to our colleagues on the program committee and the external reviewers, whose careful reviews and thoughtful deliberations served to maintain the high quality of the conference. We extend our thanks to the authors of all submitted papers and the ITP community at large, without which the conference would not exist.

Finally, we are grateful for Springer for once again publishing these proceedings as a volume in the LNCS series, and we thank the editorial team for the smooth interactions.