ITP 2017

8th International Conference on Interactive Theorem Proving (ITP 2017)

GENERAL INFORMATION
The ITP conference series is concerned with all topics related to interactive theorem proving, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and formalization of mathematics. ITP is the evolution of the TPHOLs conference series to the broad field of interactive theorem proving. TPHOLs meetings took place every year from 1988 until 2009. The eighth ITP conference, ITP 2017, will be held at Universidade de Brasilia, September 26-29, 2017.

SCOPE OF CONFERENCE
ITP welcomes submissions describing original research on all aspects of interactive theorem proving and its applications. Suggested topics include but are not limited to the following:

* formal aspects of hardware and software
* formalizations of mathematics
* improvements in theorem prover technology
* user interfaces for interactive theorem provers
* formalizations of computational models
* verification of security algorithms
* use of theorem provers in education
* industrial applications of interactive theorem provers
* concise and elegant worked examples of formalizations (proof pearls)

INVITED SPEAKERS
Moa Johansson, Chalmers University of Technology, Sweden
Leonardo de Moura, Microsoft Research
Cezary Kaliszyk, Universitaet Innsbruck, Austria (joint with TABLEAUX and FroCos)
Katalin Bimbo, University of Alberta, Canada (joint with TABLEAUX and FroCos)
Jasmin Blanchette, Inria and LORIA, Nancy, France (joint with TABLEAUX and FroCos)

WORKSHOPS AND TUTORIALS
There will be a three-day programme of four workshops and four
tutorials from 23-25 September.

Workshops:
12th Logical and Semantic Frameworks with Applications (LSFA 2017)
Sandra Alves, Renata Wassermann, Flavio L. C. de Moura
23 and 24 September 2017

Proof eXchange for Theorem Proving (PxTP)
Catherine Dubois, Bruno Woltzenlogel Paleo
23 and 24 September 2017

EPS - Encyclopedia of Proof Systems
Giselle Reis, Bruno Woltzenlogel Paleo
24 and 25 September 2017

DaLi - Dynamic Logic: new trends and applications
Mario Benevides, Alexandre Madeira
24 September 2017

Tutorials:

General methods in proof theory for modal and substructural logics
Bjoern Lellmann, Revantha Ramanayake
23 September 2017

From proof systems to complexity bounds
Anupam Das
24 September 2017

Proof Compressions and the conjecture NP =3D PSPACE
Lew Gordeev, Edward Hermann Haeusler
25 September 2017

PVS for Computer Scientists
Cesar Munoz, Mauricio Ayala-Rincon, Mariano Moscato
25 September 2017

Details will be published in separate calls and on the conference
website.

PROGRAM COMMITTEE CHAIRS
Mauricio Ayala-Rincon, U. Brasilia
Cesar Munoz, NASA

PROGRAM COMMITTEE
Maria Alpuente, T.U. Valencia
Vander Alves, U. Brasilia
June Andronick, Data61, CSIRO, UNSW
Jeremy Avigad, Carnegie Mellon U.
Sylvie Boldo, INRIA LRI
Ana Bove, Chalmers & Gothenburg U.
Adam Chlipala, MIT
Gilles Dowek, INRIA, ENS Cachan
Aaron Dutle, NASA
Amy Felty, U. Ottawa
Marcelo Frias, I.T. Buenos Aires
Ruben Gamboa, U. Wyoming
Herman Geuvers, Radboud U.
Elsa Gunter, U. Illinois U.C.
John Harrison, Intel Corporation
Nao Hirokawa, JAIST
Matt Kaufmann, U. Texas Austin
Mark Lawford, McMaster U.
Andreas Lochbihler, ETH Zurich
Assia Mahboubi, INRIA
Panagiotis Manolios, Northeastern U.
Gopalan Nadathur, U. Minnesota
Keiko Nakata, SAP Potsdam
Adam Naumowicz, U. Bialystok
Tobias Nipkow, T.U. Munich
Scott Owens, U. Kent
Sam Owre, SRI
Lawrence Paulson, U. Cambridge
Leila Ribeiro, U.F. Rio Grande do Sul
Claudio Sacerdoti Coen, U. Bologna
Augusto Sampaio, U.F. Pernambuco
Monika Seisenberger, Swansea U.
Christian Sternagel, U. Innsbruck
Sofiene Tahar, Concordia U.
Christian Urban, King's College London
Josef Urban, Czech T.U. Prague

CONTACT INFORMATION
itp2017@easychair.org
http://itp2017.cic.unb.br