[logic-ml] ITP 2017 - Final Call for Papers

[Nao Hirokawa]

皆様

ITP 2017 の論文募集案内（最終）をお送り致します。
ぜひ論文投稿をご検討下さい。

廣川 (JAIST)

----------------------------------------------------------------------

                        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