<html>
  <head>
    <meta http-equiv="content-type" content="text/html; charset=utf-8">
  </head>
  <body bgcolor="#FFFFFF" text="#000000">
    <div>                        FIRST CALL FOR PAPERS</div>
    <div><br>
    </div>
    <div>                                  ITP 2017</div>
    <div>8th International Conference on Interactive Theorem Proving</div>
    <div>                                 Brasilia, Brazil</div>
    <div>                          September 26-29, 2017</div>
    <div>                         <a href="http://itp2017.cic.unb.br">http://itp2017.cic.unb.br</a></div>
    <div><br>
    </div>
    <div><br>
    </div>
    <div>Submission Deadlines: April 3, 2017 (abstracts) </div>
    <div>                      April 10, 2017 (full papers)</div>
    <div><br>
    </div>
    <div>GENERAL INFORMATION</div>
    <div>The ITP conference series is concerned with all topics related
      to</div>
    <div>interactive theorem proving, ranging from theoretical
      foundations to</div>
    <div>implementation aspects and applications in program
      verification,</div>
    <div>security, and formalization of mathematics. ITP is the
      evolution of</div>
    <div>the TPHOLs conference series to the broad field of interactive
      theorem</div>
    <div>proving. TPHOLs meetings took place every year from 1988 until</div>
    <div>2009. The eighth ITP conference, ITP 2017, will be held at</div>
    <div>Universidade de Brasilia, September 26-29, 2017.</div>
    <div><br>
    </div>
    <div>SCOPE OF CONFERENCE </div>
    <div>ITP welcomes submissions describing original research on all
      aspects</div>
    <div>of interactive theorem proving and its applications. Suggested
      topics</div>
    <div>include but are not limited to the following: </div>
    <div><br>
    </div>
    <div>*  formal aspects of hardware and software</div>
    <div>*  formalizations of mathematics</div>
    <div>*  improvements in theorem prover technology</div>
    <div>*  user interfaces for interactive theorem provers</div>
    <div>*  formalizations of computational models</div>
    <div>*  verification of security algorithms</div>
    <div>*  use of theorem provers in education</div>
    <div>*  industrial applications of interactive theorem provers</div>
    <div>*  concise and elegant worked examples of formalizations (proof
      pearls)</div>
    <div><br>
    </div>
    <div>PUBLICATION DETAILS</div>
    <div>The proceedings of the symposium will be published in the</div>
    <div>Springer's LNCS series.</div>
    <div><br>
    </div>
    <div>PAPER SUBMISSIONS</div>
    <div>All submissions must be original, unpublished, and not
      submitted</div>
    <div>concurrently for publication elsewhere. Furthermore, when
      appropriate,</div>
    <div>submissions are expected to be accompanied by verifiable
      evidence of</div>
    <div>a suitable implementation, such as the source files of a
      formalization </div>
    <div>for the proof assistant used. Submissions should be no more
      than </div>
    <div>16 pages in length and are to be submitted in PDF via EasyChair
      at </div>
    <div>the following address:</div>
    <div><br>
    </div>
    <div>  <a href="https://easychair.org/conferences/?conf=itp2017">https://easychair.org/conferences/?conf=itp2017</a></div>
    <div><br>
    </div>
    <div>Submissions must conform to the LNCS style in LaTeX. Authors of</div>
    <div>accepted papers are expected to present their paper at the
      conference</div>
    <div>and will be required to sign a copyright release form.</div>
    <div> </div>
    <div>In addition to regular papers, described above, there will be a
      rough</div>
    <div>diamond section. Rough diamond submissions are limited to 6
      pages </div>
    <div>and may consist of an extended abstract. They will be refereed
      and be</div>
    <div>expected to present innovative and promising ideas, possibly in
      an</div>
    <div>early form and without supporting evidence. Accepted diamonds
      will be</div>
    <div>published in the main proceedings and will be presented as
      short</div>
    <div>talks.</div>
    <div><br>
    </div>
    <div>IMPORTANT DATES </div>
    <div>Abstract submission deadline: April 3, 2017</div>
    <div>Full paper submission deadline: April 10, 2017</div>
    <div>Author notification:  June 2, 2017</div>
    <div>Camera-ready papers:  June 30, 2017</div>
    <div>Workshops &amp; Tutorials:  September 23-25, 2017</div>
    <div>Conference:  September 26-29, 2017</div>
    <div><br>
    </div>
    <div>PROGRAM COMMITTEE</div>
    <div>Maria Alpuente, T.U. Valencia </div>
    <div>Vander Alves, U.  Brasilia </div>
    <div>June Andronick, U. New South Wales </div>
    <div>Jeremy Avigad, Carnegie Mellon U. </div>
    <div>Mauricio Ayala-Rincon, U. Brasilia (Co-Chair)  </div>
    <div>Sylvie Boldo, INRIA LRI </div>
    <div>Ana Bove, Chalmers &amp; Gothenburg U. </div>
    <div>Adam Chlipala, MIT </div>
    <div>Gilles Dowek, INRIA, ENS Cachan </div>
    <div>Aaron Dutle, NASA  </div>
    <div>Amy Felty, U. Ottawa </div>
    <div>Marcelo Frias, I.T. Buenos Aires</div>
    <div>Ruben Gamboa, U. Wyoming </div>
    <div>Herman Geuvers, Radboud U.</div>
    <div>Elsa Gunter, U. Illinois U.C. </div>
    <div>John Harrison, Intel Corporation </div>
    <div>Nao Hirokawa, JAIST</div>
    <div>Matt Kaufmann, U. Texas Austin</div>
    <div>Mark Lawford, McMaster U. </div>
    <div>Andreas Lochbihler, ETH Zurich </div>
    <div>Assia Mahboubi, INRIA </div>
    <div>Panagiotis Manolios, Northeastern U. </div>
    <div>Cesar Munoz, NASA (Co-Chair)</div>
    <div>Gopalan Nadathur, U. Minnesota </div>
    <div>Keiko Nakata, T.U. Dresden </div>
    <div>Adam Naumowicz, U. Bialystok</div>
    <div>Tobias Nipkow, T.U. Munich </div>
    <div>Scott Owens, U. Kent </div>
    <div>Sam Owre, SRI</div>
    <div>Lawrence Paulson, U. Cambridge </div>
    <div>Leila Ribeiro, U.F.  Rio Grande do Sul </div>
    <div>Claudio Sacerdoti Coen, U. Bologna </div>
    <div>Augusto Sampaio, U.F. Pernambuco </div>
    <div>Monika Seisenberger, Swansea U.</div>
    <div>Christian Sternagel, U. Innsbruck </div>
    <div>Sofiene Tahar,  Concordia U.</div>
    <div>Christian Urban, King's College London </div>
    <div>Josef Urban, Czech T.U. Prague</div>
    <div><br>
    </div>
    <div>CONTACT INFORMATION </div>
    <div>Cesar Munoz</div>
    <div>Mauricio Ayala-Rincon</div>
    <div><a href="mailto:itp2017@easychair.org">itp2017@easychair.org</a></div>
    <div><a href="http://itp2017.cic.unb.br">http://itp2017.cic.unb.br</a></div>
    <div><br>
    </div>
    <br>
  </body>
</html>