皆様
９月にブラジリアで開催されます、対話的定理証明に関する国際会議 ITP 2017 の論文募集案内をお送り致します。ぜひ投稿をご検討下さい。
廣川 (JAIST)
-------------------------------------------------------------------- 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 [email protected] http://itp2017.cic.unb.br