ITP 2014
International Conference on Interactive Theorem Proving
14th-17th July 2014 in Vienna, Austria
http://www.cs.uwyo.edu/~ruben/itp-2014
CALL FOR PAPERS
IMPORTANT DATES
Abstract submission: | |
---|---|
Paper submission: | |
Author notification: | |
Camera-ready paper versions due: | |
Conference Registration: | |
Conference Dates: |
CONFERENCE BACKGROUND
ITP is the premier international conference for researchers from all areas of interactive theorem proving and its applications. It represents the natural evolution of the TPHOLs conference series to include research related to all other interactive theorem provers. TPHOLs meetings took place every year from 1988 until 2009. In 2010, the first ITP conference was held in Edinburgh, Scotland, as part of the Federated Logic Conference (FLoC). Subsequent ITP conferences were held in Nijmegen, The Netherlands, in 2011, Princeton, New Jersey, USA, in 2012, and Rennes, France in 2013. ITP 2014 will again be a part of FLoC, in Vienna, Austria.
PAPER SUBMISSIONS
ITP welcomes submissions describing original research on all aspects of interactive theorem proving and its applications. In particular, the ITP community is open to users of all interactive theorem provers. 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,
- use of theorem provers in education,
- industrial applications of interactive theorem provers, and
- concise and elegant worked examples of formalizations ("Proof Pearls").
Submissions must be made electronically in PDF format. Submissions should be prepared using the Springer LNCS format, available from http://www.springer.com/computer/lncs/lncs+authors, and submitted via EasyChair. Submissions must describe original unpublished work not submitted for publication elsewhere, presented in a way that is accessible to users of other systems. The proceedings will be published as a volume in the Springer Lecture Notes in Computer Science series and will be available to participants at the conference.
ITP accepts both long papers (up to sixteen pages) and "rough diamonds" (up to six pages, possibly in the form of an extended abstract). Both categories of papers will be fully refereed and included in the published proceedings. Papers in the "rough diamonds" category are expected to present innovative and promising ideas that have not yet had the time to mature. Regular papers are expected to present mature research projects with appropriate supporting evidence.
All papers should have an abstract of approximately 100 words. Note that abstracts must be submitted a week prior to the paper submission deadline. Papers should also include a list of relevant keywords, which must include the name of the theorem prover featured in the paper. We strongly encourage submissions that describe interactions with or improvements of a theorem prover. Authors of such papers should provide verifiable evidence of an implementation, such as appropriate source files. This material may be uploaded via EasyChair or may be placed online, as long as a URL is included with the submission.
Authors of accepted papers are expected to present their papers at the conference, and will be required to sign copyright release forms. All submissions must be written in English.
ORGANIZATION
Program Chairs
- Gerwin Klein, NICTA and The University of New South Wales, Australia
- Ruben Gamboa, University of Wyoming, USA
Workshop Chair
- David Pichardie, INRIA, France
Program Committee
- Jeremy Avigad, Carnegie Mellon University
- Lennart Beringer, Princeton University
- Yves Bertot, INRIA
- Thierry Coquand, Chalmers University
- Amy Felty, University of Ottawa
- Ruben Gamboa, University of Wyoming
- Georges Gonthier, Microsoft Research
- Elsa Gunter, Departement of Computer Science, University of Illinois at Urbana-Champaign
- John Harrison, Intel Corporation
- Matt Kaufmann, University of Texas at Austin
- Gerwin Klein, NICTA and UNSW
- Alexander Krauss, Technische Universität München
- Ramana Kumar, University of Cambridge
- Joe Leslie-Hurd, Intel Corporation
- Assia Mahboubi, INRIA - École polytechnique
- Panagiotis Manolios, Northeastern University
- Magnus O. Myreen, University of Cambridge
- Tobias Nipkow, TU München
- Michael Norrish, NICTA
- Sam Owre, SRI International
- Christine Paulin-Mohring, Université Paris-Sud
- Lawrence Paulson, University of Cambridge
- David Pichardie, INRIA Rennes - Bretagne Atlantique
- Lee Pike, Galois, Inc.
- Jose-Luis Ruiz-Reina, Departament of Computer Science and Artificial Intelligence (University of Seville)
- Julien Schmaltz, Open University of the Netherlands
- Bas Spitters, Radboud University Nijmegen
- Sofiene Tahar, Concordia University
- René Thiemann, University of Innsbruck
- Laurent Théry, INRIA
- Christian Urban
- Tjark Weber, Uppsala University
- Makarius Wenzel, Université Paris-Sud 11