26-29 Sep 2017
Brasilia, Brazil
SECOND 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.
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.
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.
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
Katalin Bimbo, University of Alberta, Canada (joint with TABLEAUX and
FroCos)
Jasmin Blanchette Inria and LORIA, Nancy, France (joint with TABLEAUX
and FroCos)
Cesary Kaliszyk Universitaet Innsbruck, Austria (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 CHAIRS
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
Cesar Munoz
Mauricio Ayala-Rincon
itp2017@easychair.org
http://itp2017.cic.unb.br
--
[LOGIC] mailing list
http://www.dvmlg.de/mailingliste.html
Archive: http://www.illc.uva.nl/LogicList/
provided by a collaboration of the DVMLG, the Maths Departments in Bonn and Hamburg, and the ILLC at the Universiteit van Amsterdam