Interactive theorem proving : second international conference, ITP 2011, Berg en Dal, The Netherlands, 22-25, 2011 : proceedings

This volume contains the papers presented at ITP 2011: the Second International Conference on Interactive Theorem Proving. It was held during August 22–25, 2011 in Berg en Dal, The Netherlands. ITP brings together researchers working in all areas of interactive theorem proving. ITP is the evolution of the TPHOLs conference series to the broad field of interactive theorem proving. The inaugural meeting of ITP was held during July 11–14, 2010 in Edinburgh, Scotland, as part of the Federated Logic Conference (FLoC, July 9–21, 2010). TPHOLs meetings took place every year from 1988 until 2009. There were 50 submissions to ITP 2011, each of which was reviewed by at least four Program Committee members. Out of the 50 submissions, 42 were regular papers and 8 were rough diamonds. The Program Committee accepted 21 regular papers, including one proof pearl and four rough diamonds. All 25 papers are included in the proceedings. The Program Committee also invited two leading researchers from Industry, Georges Gonthier (Microsoft Research) and Mike Kishinevsky (Intel Corporation), and two leading researchers from academia, Don Batory (University of Texas at Austing) and Bart Jacobs (Radboud University Nijmegen), to present invited lectures. Two system demos were given at ITP 2011. Each demo consisted in an indepth presentation of 90 minutes about the application of an ITP system on a real example. Details about the practical use of ACL2 and KeY were presented. ITP 2011 featured seven associated workshops that took place on August 26 and August 27. The workshops were the following: The Third Coq Workshop, the Third Workshop on Dependently Typed Programming, the 10th KeY Symposium, the 6th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, the ITP 2011 Workshop on Mathematical Wikis, the Third Workshop on Modules and Libraries for Proof Assistants, the 6th International Workshop on Systems Software Verification. We would like to thank our Local Chair Nicole Messink for the valuable and efficient support in planning and running ITP. We would like to thank all the local organizers for their help during the event. The work of the Program Committe and the editorial process were facilitated by the EasyChair conference management system. We are grateful to Springer for publishing these proceedings, as they have done for ITP 2010 and TPHOLs and its predecessors since 1993. Finally, we would like to thank our sponsors: The Netherlands Organisation for Scientific Research (NWO) and The Royal Netherlands Academy of Arts and Sciences (KNAW)