[fg-arc] [fm-announcements] ITP 2017 - Final Call for Papers

[Munoz, Cesar (LARC-D320)]

           *** Apologies for multiple copies, please redistribute ***

                         FINAL CALL FOR PAPERS

                                   ITP 2017
8th International Conference on Interactive Theorem Proving
                                  Brasilia, Brazil
                           September 26-29, 2017
                          http://itp2017.cic.unb.br


SUBMISSION DEADLINES
* April 3, 2017 (abstracts)
* April 10, 2017 (full papers)

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)

PUBLICATION DETAILS
The proceedings of the symposium will be published in the
Springer's LNCS series.

** After the conference the authors of selected papers will be invited
to submit revised papers for a special issue of the Journal of Automated
Reasoning.  **

PAPER SUBMISSIONS
All submissions must be original, unpublished, and not submitted
concurrently for publication elsewhere. Furthermore, when appropriate,
submissions are expected to be accompanied by verifiable evidence of
a suitable implementation, such as the source files of a formalization
for the proof assistant used. Submissions should be no more than
16 pages in length and are to be submitted in PDF via EasyChair at
the following address:

   https://easychair.org/conferences/?conf=itp2017

Submissions must conform to the LNCS style in LaTeX. Authors of
accepted papers are expected to present their paper at the conference
and will be required to a sign copyright release form.

In addition to regular papers, described above, there will be a rough
diamond section. Rough diamond submissions are limited to 6 pages
and may consist of an extended abstract. They will be refereed and be
expected to present innovative and promising ideas, possibly in an
early form and without supporting evidence. Accepted diamonds will be
published in the main proceedings and will be presented as short
talks.

IMPORTANT DATES
Abstract submission deadline: April 3, 2017
Full paper submission deadline: April 10, 2017
Author notification:  June 2, 2017
Camera-ready papers:  June 30, 2017
Workshops & Tutorials:  September 23-25, 2017
Conference:  September 26-29, 2017

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 at easychair.org
http://itp2017.cic.unb.br




---
To opt-out from this mailing list, send an email to

fm-announcements-request at lists.nasa.gov

with the word 'unsubscribe' as subject or in the body. You can also make the request by contacting

fm-announcements-owner at lists.nasa.gov