<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 & 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 & 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>