[FM-India] Call for Papers: ITP 2014

[Madhavan Mukund]

 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