[FM-India] Call for Papers: ITP 2014
Madhavan Mukund
madhavan at cmi.ac.in
Fri Dec 20 17:26:12 IST 2013
From: Gerwin Klein <gerwin.klein at nicta.com.au>
To: fmindia at cmi.ac.in
Date: Fri, 20 Dec 2013 21:13:54 +1100
Subject: Call for Papers: ITP 2014
Call for Papers
ITP 2014
5th International Conference on Interactive Theorem Proving
14th-17th July 2014 in Vienna, Austria
http://www.cs.uwyo.edu/~ruben/itp-2014
IMPORTANT DATES
Abstract submission: 24th January 2014
Paper submission: 31st January 2014
Author notification: 21st March 2014
Camera-ready: 18th April 2014
Conference: 14th-17th July 2014
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 16 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, 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, 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, King's College London
Tjark Weber, Uppsala University
Makarius Wenzel, Université Paris-Sud 11
More information about the FMIndia
mailing list