[TYPES/announce] ITP 2013: First Call for Papers

[David Pichardie]

ITP 2013: 4th International Conference on Interactive Theorem Proving

                  23-26 July 2013, Rennes, France
                      http://itp2013.inria.fr

ITP is the premier international conference for researchers from all
areas of interactive theorem proving and its applications. The
inaugural meeting of ITP was held in July 2010 in Edinburgh, Scotland,
as part of the Federated Logic Conference (FLoC), the second
meeting took place in Nijmegen, The Netherlands, in August 2011 and
the third meeting was held in Princeton, New Jersey, in  August 2012. 
ITP 2013 will take place in Rennes, France on 23-26 July
2013 with workshops preceding the main conference.  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 program committee welcomes submissions on all aspects of
interactive theorem proving and its applications.  Examples of typical
topics include formal aspects of hardware or software (specification,
verification, semantics, synthesis, refinement, compilation, etc.);
formalization of significant bodies of mathematics; advances in
theorem prover technology (automation, decision procedures, induction,
combinations of systems and tools, etc.); other topics including those
relating to user interfaces, education, comparisons of systems, and
mechanizable logics; and concise and elegant worked examples ("Proof
Pearls").

Submission details:

All papers must be submitted electronically, via EasyChair:
https://www.easychair.org/conferences/?conf=itp2013

Papers may be no longer than 16 pages and are to be submitted in PDF
using the Springer "llncs" format.  Instructions may be found at
ftp://ftp.springer.de/pub/tex/latex/llncs/latex2e/instruct/authors/typeinst.pdf
with Latex source file typeinst.tex in the same directory.
Submissions must describe original unpublished work not submitted for
publication elsewhere, presented in a way that users of other systems
can understand.  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.

In addition to regular submissions, described above, there will be a
"rough diamonds" section.  Rough diamond submissions are limited to
six pages and may consist of an extended abstract.  They will be
refereed: they will 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.

Both regular and rough diamond submissions require an abstract of 70
to 150 words to be submitted electronically at the above address one
week before the full submission.  All submissions must be written in
English.  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. Details on how to submit 
will be forthcoming. Authors who have strong reasons (e.g. of 
commercial/legal nature) for violating this policy should contact the
PC chairs in advance. At the time of abstract submission, proof 
assistants and other tools necessary for evaluating the submission 
should be indicated using the Keywords section of the web interface.

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.

Important dates:

Abstract submission deadline:           28 January 2013
Paper submission deadline:              1st February 2013
Notification of paper decisions:        28 March 2013
Final versions due from authors:        22 April 2013
Conference dates:                       23-26 July 2013

Web page: http://itp2013.inria.fr

Program Committee:
Wolfgang Ahrendt, Chalmers University, Sweden
Jeremy Avigad, Carnegie Mellon University, USA
Nick Benton, Microsoft Research, UK
Lennart Beringer, Princeton University, USA
Sandrine Blazy, University of Rennes, France (co-chair)
Adam Chlipala, MIT, USA
Thierry Coquand, Chalmers University, Sweden
Amy Felty, University of Ottawa, Canada
Ruben Gamboa, University of Wyoming, USA
Herman Geuvers, Radboud University Nijmegen, The Netherlands
Elsa Gunter, University of Illinois at Urbana-Champaign, USA
David Hardin, Rockwell Collins, Inc., USA
John Harrison, Intel Corporation, USA
Gerwin Klein, NICTA and UNSW, Australia
Assia Mahboubi, INRIA - École polytechnique, France
Panagiotis Manolios, Northeastern University, USA
Conor Mcbride, University of Strathclyde, UK
César Muñoz, NASA, USA
Magnus O. Myreen, University of Cambridge, UK
Tobias Nipkow, TU München, Germany
Michael Norrish, NICTA and ANU, Australia
Sam Owre, SRI International, USA
Christine Paulin-Mohring, Université Paris-Sud 11, France (co-chair)
Lawrence Paulson, University of Cambridge, UK
David Pichardie, Inria Rennes/Harvard University, France (co-chair)
Brigitte Pientka, McGill University, Canada
Laurence Pierre, TIMA, France
Lee Pike, Galois, Inc., USA
Claudio Sacerdoti Coen, University of Bologna, Italy
Julien Schmaltz, Open University of the Netherlands, The Netherlands
Makoto Takeyama, AIST/COVS, Japan
Laurent Théry, Inria Sophia-Antipolis, France
René Thiemann, University of Innsbruck, Austria
Makarius Wenzel, Université Paris-Sud 11, France

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20121126/cd6f62a2/attachment.html>