[TYPES/announce] ITP 2012: Final Call for Papers

[Amy Felty]

                        Final Call for Papers
ITP 2012: 3rd International Conference on Interactive Theorem Proving

           13-16 August 2012, Princeton, New Jersey, USA
                    http://itp2012.cs.princeton.edu/

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), and the second
meeting took place in Nijmegen, The Netherlands, in August 2011.  ITP
2012 will take place in Princeton, New Jersey, USA on 13-16 August
2012 with two workshops preceding the main conference: The Isabelle
Workshop 2012 (organized by Tobias Nipkow, Larry Paulson, and Makarius
Wenzel) and the 4th Coq Workshop (organized by Adam Chlipala).  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.); industrial applications of
theorem proving; 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=itp2012

Papers may be no longer than 16 pages and are to be submitted in PDF
using the Springer LNCS format.  Instructions and style files may be
found by going to http://www.springer.com/computer/lncs/lncs+authors
and downloading the files llncs2e.zip and typeinst.zip.  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 and are 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.  The submission page
contains a corresponding file upload function.  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.

Important dates:

Abstract submission deadline:           6 February 2012
Paper submission deadline:              13 February 2012
Notification of paper decisions:        13 April 2012
Final versions due from authors:        5 May 2012
Pre-conference workshops:               12 August 2012
Conference dates:                       13-16 August 2012

Web page: http://itp2012.cs.princeton.edu/

Invited Speakers:
Gilles Barthe (IMDEA, Spain)
Lawrence Paulson (Univ. of Cambridge, UK)
Andre Platzer (Carnegie Mellon Univ., USA)

Invited Tutorial:
Andrew Gacek (Rockwell Collins, USA)

General Co-Chairs:
Andrew Appel (Princeton Univ., USA)
Lennart Beringer (Princeton Univ., USA)

Program Co-Chairs:
Lennart Beringer (Princeton Univ., USA)
Amy Felty (Univ. of Ottawa, Canada)

Program Committee:
Andreas Abel (LMU Munich, Germany)
Nick Benton (Microsoft Research Cambridge, UK)
Stefan Berghofer (secunet Security Networks AG, Germany)
Lennart Beringer (Co-Chair, Princeton Univ., USA)
Yves Bertot (INRIA Sophia-Antipolis, France)
Adam Chlipala (MIT, USA)
Ewen Denney (NASA, USA)
Peter Dybjer (Chalmers Univ. of Technology, Sweden)
Amy Felty (Co-Chair, Univ. of Ottawa, Canada)
Herman Geuvers (Radboud Univ. Nijmegen, The Netherlands)
Georges Gonthier (Microsoft Research Cambridge, UK)
Jim Grundy (Intel Corp., USA)
Elsa Gunter (Univ. Illinois at Urbana-Champaign, USA)
Hugo Herbelin (INRIA Roquencourt-Paris, France)
Joe Hurd (Galois, Inc., USA)
Reiner Hähnle (Chalmers Univ. of Technology, Sweden)
Matt Kaufmann (Univ. of Texas at Austin, USA)
Gerwin Klein (NICTA, Australia)
Assia Mahboubi (INRIA Saclay, France)
Conor McBride (Univ. of Strathclyde, UK)
Alberto Momigliano (Univ. of Milan, Italy)
Magnus O. Myreen (Univ. of Cambridge, UK)
Tobias Nipkow (TU Munich, Germany)
Sam Owre (SRI, USA)
Christine Paulin-Mohring (Univ. Paris-Sud, France)
David Pichardie (INRIA Rennes, France)
Brigitte Pientka (McGill Univ., Canada)
Randy Pollack (Harvard Univ., USA)
Julien Schmaltz (Open Univ. of the Netherlands, The Netherlands)
Bas Spitters (Radboud Univ. Nijmegen, The Netherlands)
Sofiene Tahar (Concordia Univ., Canada)
Makarius Wenzel (Univ. Paris-Sud, France)