ITP 2013 is the fourth conference on Interactive Theorem Proving and related issues, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and formalization of mathematics. 



Applying formal methods in the largeDominique Bolignano (Prove and Run), Tuesday 23rd July 2013 
Automating theorem proving with SMTRustan Leino (Microsoft Research), Wednesday 24th July 2013 
Certifying voting protocolsCarsten Schürmann (University of Copenhagen), Friday 25th July 2013 

Counterexample Generation Meets Interactive Theorem Proving: Current Results and Future OpportunitiesPete Manolios (Northeastern University), Tuesday 23rd July 2013 
The Mathematical Components library  principles and design choicesAssia Mahmoudi & Enrico Tassi (Microsoft Research Inria Joint Center), Wednesday 24th July 2013 