The CELTIQUE and ProVal teams of INRIA offer to host ITP 2013, the International Conference on Interactive Theorem Proving in Rennes, France. Rennes offers excellent facilities and settings for hosting ITP 2013, and the INRIA research centre has a long tradition in the organization of international conferences. Last but not least, Rennes is Brittany's capital city; Brittany is of a well-known touristic region with world-class attractions (such as the Mont Saint-Michel, Saint Malo corsair city). Rennes is a medium size city. It is located two hours away from Paris by the TGV (high-speed) train. Rennes runs an international airport located close to the city, with direct connections to most French cities, and optimized flight connection with most European cities. The conference venue will be a brand new conference centre built inside the INRIA premises. This is key to keep registration costs as low as possible, while taking advantage of the exciting life of this very dynamic city. The CELTIQUE and ProVal teams participate to the INRIA major scientific priorities: “Programming: Security and Reliability of Computing Systems”. Both teams are developing a strong expertise in different fields that are relevant to the ITP community: program proof, decision procedures, formal verification of floating-point arithmetic, formal verification of compilers and static analyzers.