ITP 2014 LNCS PROCEEDINGS: EDITOR'S PREFACE

This volume contains the papers presented at ITP 2014: 5th International Conference on Interactive Theorem Proving held on July 13-16, 2014 in Vienna, as part of the Federated Logic Conference (FLoC, July 10-24, 2014), which was part of the Vienna Summer of Logic (July 9-24, 2014).

ITP 2014 was the fifth conference on Interactive Theorem Proving and related areas, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and formalization of mathematics. The inaugural meeting of ITP was held on 11-14 July 2010 in Edinburgh, Scotland, as part of the Federated Logic Conference (FLoC, 9-21 July 2010).  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.

There were 59 submissions to ITP 2014, each of which was reviewed by at least 3 program committee members. The committee decided to accept 35 papers, 4 of which were rough diamonds. The program also includes invited talks by Anna Slobodova, Rod Chapman, and Peter Sewell.

We would like to thank the co-chairs of the Vienna Summer of Logic (Matthias Baaz, Thomas Eiter, Helmut Veith), the FLoC general chair (Moshe Vardi), all the other members of the VSL and FLoC organizing committee, and David Pichardie, who was kind enough to take care of ITP's satellite workshops. We gratefully acknowledge the support of VSL's partners and sponsors, including TU Wien, IST Austria, Universitat Wien, StaDt Wien, Austrian Airlines, the Federal Ministry of Science Research and Economy, the University of Manchester, Cateringkultur, Vienna Convention Bureau, Elsevier's Artificial Intelligence, European Association for Computer Science Logic, Blacklane Limousines, Fraunhofer, OrbiTeam, Rigorous Systems Engineering, and College Publications.  We also gratefully ackowledge the support of FLoC's sponsors: Microsoft Research, ARM, and NEC. And we extend a special thanks to ITP's sponsors: NICTA, and HappyJack Software.

Next year's conference will be held in Nanjing, China. The site was chosen by the ITP Steering Committee in consultation with the broader ITP community.