This book constitutes the refereed proceedings of the 4th International Conference on Interactive Theorem Proving, ITP 2013, held in Rennes, France, in July 2013. The 26 regular full papers presented together with 7 rough diamond papers, 3 invited talks, and 2 invited tutorials were carefully reviewed and selected from 66 submissions. The papers are organized in topical sections such as program verfication, security, formalization of mathematics and theorem prover development.

ThisvolumecontainstheproceedingsofMPC2008, the9thInternationalConf- enceontheMathematicsofProgramConstruction.Thisseriesofconferencesaims to promote the development of mathematical principles and techniques that are demonstrably useful in the process of constructing computer programs, whether implemented in hardware or software. The focus is on techniques that combine precision with conciseness, enabling programs to be constructed by formal c- culation.Within this theme, the scopeofthe seriesisverydiverse, including p- grammingmethodology, programspeci?cationandtransformation, programming paradigms, programmingcalculi, andprogramminglanguagesemantics. The quality of the papers submitted to the conference was in general very high, and the number of submissions was comparable to that for the previous conference. Each paper was refereed by at least four, and often more, committee members. This volume contains 18 papers selected for presentation by the Program Committee from 41 submissions, 1 invited paper which was reviewed as well, and the abstracts for two invited talks. The conference took place in Marseille-Luminy, France. The previous eight conferences were held in 1989 in Twente, The Netherlands; in 1992 in Oxford, UK; in 1995 in Kloster Irsee, Germany; in 1998 in Marstrand near Got ] eborg, Sweden; in 2000 in Ponte de Lima, Portugal; in 2002 in Dagstuhl, Germany; in 2004, in Stirling, UK; and in 2006 in Kuressaare, Estonia. The proceedings of these conferences were published as LNCS 375, 669, 947, 1422, 1837, 2386, 3125 and 4014, respectively. We aregratefulto the members ofthe ProgramCommittee andtheir referees for their care and diligence in reviewing the submitted pa

The 17 revised full papers presented here cover all current issues of formal reasoning and computer programming based on type theory are addressed; in particular languages and computerised tools for reasoning, and applications in several domains such as analysis of programming languages, certified software, formalisation of mathematics and mathematics education.

This book constitutes the thoroughly revised post-workshop proceedings of the first annual workshop held under the auspices of the ESPRIT Working Group 21900 TYPES in Aussois, France in December 1996.
The 18 revised full papers presented in the book were carefully reviewed and selected from the 30 papers accepted for presentation at the workshop. All current aspects of type theory and type systems and their applications to program verification and theorem proving are addressed; the proof systems and theorem provers dealt with include Coq, LEGO, and Isabelle/HOL.