<html><head><meta http-equiv="Content-Type" content="text/html charset=iso-8859-1"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div><div><font face="Monaco">ITP 2013: 4th International Conference on Interactive Theorem Proving</font></div><div><font face="Monaco"><br></font></div><div><font face="Monaco"> 23-26 July 2013, Rennes, France</font></div><div><font face="Monaco"> <a href="http://itp2013.inria.fr">http://itp2013.inria.fr</a></font></div><div><font face="Monaco"><br></font></div><div><font face="Monaco">ITP is the premier international conference for researchers from all</font></div><div><font face="Monaco">areas of interactive theorem proving and its applications. The</font></div><div><font face="Monaco">inaugural meeting of ITP was held in July 2010 in Edinburgh, Scotland,</font></div><div><font face="Monaco">as part of the Federated Logic Conference (FLoC), the second</font></div><div><font face="Monaco">meeting took place in Nijmegen, The Netherlands, in August 2011 and</font></div><div><font face="Monaco">the third meeting was held in Princeton, New Jersey, in August 2012. </font></div><div><font face="Monaco">ITP 2013 will take place in Rennes, France on 23-26 July</font></div><div><font face="Monaco">2013 with workshops preceding the main conference. ITP is the</font></div><div><font face="Monaco">evolution of the TPHOLs conference series to the broad field of</font></div><div><font face="Monaco">interactive theorem proving. TPHOLs meetings took place every year</font></div><div><font face="Monaco">from 1988 until 2009.</font></div><div><font face="Monaco"><br></font></div><div><font face="Monaco">The program committee welcomes submissions on all aspects of</font></div><div><font face="Monaco">interactive theorem proving and its applications. Examples of typical</font></div><div><font face="Monaco">topics include formal aspects of hardware or software (specification,</font></div><div><font face="Monaco">verification, semantics, synthesis, refinement, compilation, etc.);</font></div><div><font face="Monaco">formalization of significant bodies of mathematics; advances in</font></div><div><font face="Monaco">theorem prover technology (automation, decision procedures, induction,</font></div><div><font face="Monaco">combinations of systems and tools, etc.); other topics including those</font></div><div><font face="Monaco">relating to user interfaces, education, comparisons of systems, and</font></div><div><font face="Monaco">mechanizable logics; and concise and elegant worked examples ("Proof</font></div><div><font face="Monaco">Pearls").</font></div><div><font face="Monaco"><br></font></div><div><font face="Monaco">Submission details:</font></div><div><font face="Monaco"><br></font></div><div><font face="Monaco">All papers must be submitted electronically, via EasyChair:</font></div><div><font face="Monaco"><a href="https://www.easychair.org/conferences/?conf=itp2013">https://www.easychair.org/conferences/?conf=itp2013</a></font></div><div><font face="Monaco"><br></font></div><div><font face="Monaco">Papers may be no longer than 16 pages and are to be submitted in PDF</font></div><div><font face="Monaco">using the Springer "llncs" format. Instructions may be found at</font></div><div><font face="Monaco"><a href="ftp://ftp.springer.de/pub/tex/latex/llncs/latex2e/instruct/authors/typeinst.pdf">ftp://ftp.springer.de/pub/tex/latex/llncs/latex2e/instruct/authors/typeinst.pdf</a></font></div><div><font face="Monaco">with Latex source file typeinst.tex in the same directory.</font></div><div><font face="Monaco">Submissions must describe original unpublished work not submitted for</font></div><div><font face="Monaco">publication elsewhere, presented in a way that users of other systems</font></div><div><font face="Monaco">can understand. The proceedings will be published as a volume in the</font></div><div><font face="Monaco">Springer Lecture Notes in Computer Science series and will be</font></div><div><font face="Monaco">available to participants at the conference.</font></div><div><font face="Monaco"><br></font></div><div><font face="Monaco">In addition to regular submissions, described above, there will be a</font></div><div><font face="Monaco">"rough diamonds" section. Rough diamond submissions are limited to</font></div><div><font face="Monaco">six pages and may consist of an extended abstract. They will be</font></div><div><font face="Monaco">refereed: they will be expected to present innovative and promising</font></div><div><font face="Monaco">ideas, possibly in an early form and without supporting evidence.</font></div><div><font face="Monaco">Accepted diamonds will be published in the main proceedings, and will</font></div><div><font face="Monaco">be presented as short talks.</font></div><div><font face="Monaco"><br></font></div><div><font face="Monaco">Both regular and rough diamond submissions require an abstract of 70</font></div><div><font face="Monaco">to 150 words to be submitted electronically at the above address one</font></div><div><font face="Monaco">week before the full submission. All submissions must be written in</font></div><div><font face="Monaco">English. Submissions are expected to be accompanied by verifiable</font></div><div><font face="Monaco">evidence of a suitable implementation, such as the source files of a</font></div><div><font face="Monaco">formalization for the proof assistant used. Details on how to submit </font></div><div><font face="Monaco">will be forthcoming. Authors who have strong reasons (e.g. of </font></div><div><font face="Monaco">commercial/legal nature) for violating this policy should contact the</font></div><div><font face="Monaco">PC chairs in advance. At the time of abstract submission, proof </font></div><div><font face="Monaco">assistants and other tools necessary for evaluating the submission </font></div><div><font face="Monaco">should be indicated using the Keywords section of the web interface.</font></div><div><font face="Monaco"><br></font></div><div><font face="Monaco">Authors of accepted papers are expected to present their papers at the</font></div><div><font face="Monaco">conference, and will be required to sign copyright release forms. </font></div><div><font face="Monaco">All submissions must be written in English.</font></div><div><font face="Monaco"><br></font></div><div><font face="Monaco">Important dates:</font></div><div><font face="Monaco"><br></font></div><div><font face="Monaco">Abstract submission deadline: 28 January 2013</font></div><div><font face="Monaco">Paper submission deadline: 1st February 2013</font></div><div><font face="Monaco">Notification of paper decisions: 28 March 2013</font></div><div><font face="Monaco">Final versions due from authors: 22 April 2013</font></div><div><font face="Monaco">Conference dates: 23-26 July 2013</font></div><div><font face="Monaco"><br></font></div><div><font face="Monaco">Web page: <a href="http://itp2013.inria.fr">http://itp2013.inria.fr</a></font></div><div><font face="Monaco"><br></font></div><div><font face="Monaco">Program Committee:</font></div><div><font face="Monaco">Wolfgang Ahrendt, Chalmers University, Sweden</font></div><div><font face="Monaco">Jeremy Avigad, Carnegie Mellon University, USA</font></div><div><font face="Monaco">Nick Benton, Microsoft Research, UK</font></div><div><font face="Monaco">Lennart Beringer, Princeton University, USA</font></div><div><font face="Monaco">Sandrine Blazy, University of Rennes, France (co-chair)</font></div><div><font face="Monaco">Adam Chlipala, MIT, USA</font></div><div><font face="Monaco">Thierry Coquand, Chalmers University, Sweden</font></div><div><font face="Monaco">Amy Felty, University of Ottawa, Canada</font></div><div><font face="Monaco">Ruben Gamboa, University of Wyoming, USA</font></div><div><font face="Monaco">Herman Geuvers, Radboud University Nijmegen, The Netherlands</font></div><div><font face="Monaco">Elsa Gunter, University of Illinois at Urbana-Champaign, USA</font></div><div><font face="Monaco">David Hardin, Rockwell Collins, Inc., USA</font></div><div><font face="Monaco">John Harrison, Intel Corporation, USA</font></div><div><font face="Monaco">Gerwin Klein, NICTA and UNSW, Australia</font></div><div><font face="Monaco">Assia Mahboubi, INRIA - École polytechnique, France</font></div><div><font face="Monaco">Panagiotis Manolios, Northeastern University, USA</font></div><div><font face="Monaco">Conor Mcbride, University of Strathclyde, UK</font></div><div><font face="Monaco">César Muñoz, NASA, USA</font></div><div><font face="Monaco">Magnus O. Myreen, University of Cambridge, UK</font></div><div><font face="Monaco">Tobias Nipkow, TU München, Germany</font></div><div><font face="Monaco">Michael Norrish, NICTA and ANU, Australia</font></div><div><font face="Monaco">Sam Owre, SRI International, USA</font></div><div><font face="Monaco">Christine Paulin-Mohring, Université Paris-Sud 11, France (co-chair)</font></div><div><font face="Monaco">Lawrence Paulson, University of Cambridge, UK</font></div><div><font face="Monaco">David Pichardie, Inria Rennes/Harvard University, France (co-chair)</font></div><div><font face="Monaco">Brigitte Pientka, McGill University, Canada</font></div><div><font face="Monaco">Laurence Pierre, TIMA, France</font></div><div><font face="Monaco">Lee Pike, Galois, Inc., USA</font></div><div><font face="Monaco">Claudio Sacerdoti Coen, University of Bologna, Italy</font></div><div><font face="Monaco">Julien Schmaltz, Open University of the Netherlands, The Netherlands</font></div><div><font face="Monaco">Makoto Takeyama, AIST/COVS, Japan</font></div><div><font face="Monaco">Laurent Théry, Inria Sophia-Antipolis, France</font></div><div><font face="Monaco">René Thiemann, University of Innsbruck, Austria</font></div><div><font face="Monaco">Makarius Wenzel, Université Paris-Sud 11, France</font></div></div><div><br></div></body></html>