ITP 2010: Call for Papers

ITP 2010 - International Conference on Interactive Theorem Proving

Edinburgh, UK, July 11-14, 2010

Important dates (midnight GMT):

Conference scope:

ITP brings together researchers working in all areas of interactive theorem proving. It combines the communities of two venerable meetings: the TPHOLs conference and the ACL2 workshop. The inaugural meeting of ITP will be held on 11-14 July 2010 in Edinburgh, Scotland, as part of the Federated Logic Conference (FLoC, 9-21 July 2010), co-located with the other FLoC conferences (CAV, ICLP, IJCAR, LICS, RTA, SAT) and workshops.

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.

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 four 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. They will be presented at the conference venue in a poster session.

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.

Program Chairs

Matt Kaufmann, University of Texas at Austin, United States
Lawrence Paulson, University of Cambridge, United Kingdom

Program Committee:

Thorsten Altenkirch, Uni Nottingham, United Kingdom
David Aspinall, University of Edinburgh, United Kingdom
Jeremy Avigad, Carnegie Mellon University, United States
Gilles Barthe, IMDEA Software, Spain
Jens Brandt, University of Kaiserslautern, Germany
Thierry Coquand, Chalmers University, Sweden
Ruben Gamboa, University of Wyoming, United States
Georges Gonthier, Microsoft Research, United Kingdom
David Greve, Rockwell Collins, United States
Elsa Gunter, Departement of Computer Science, University of Illinois at Urbana-Champaign, United States
John Harrison, Intel Corporation, United States
Joe Hurd, Galois, Inc., United States
Gerwin Klein, NICTA and UNSW, Australia
Xavier Leroy, INRIA Paris-Rocquencourt, France
Assia Mahboubi, INRIA Saclay -- Île - de - France, France
Panagiotis Manolios, Northeastern University, United States
John Matthews, Galois Connections, Inc., United States
J Moore, University of Texas at Austin, United States
Cesar Munoz, National Aeronautics and Space Administration, United States
Tobias Nipkow, TU Munich, Germany
Michael Norrish, NICTA, Australia
David Pichardie, INRIA Rennes - Bretagne Atlantique, France
Brigitte Pientka, McGill University, Canada
Lee Pike, Galois, Inc., United States
Sandip Ray, University of Texas at Austin, United States
Jose-Luis Ruiz-Reina, Departament of Computer Science (University of Seville), Spain
David Russinoff, AMD, United States
Peter Sewell, Computer Laboratory, University of Cambridge, United Kingdom
Konrad Slind
Sofiene Tahar, Concordia University, Canada
Christian Urban, TU Munich, Germany

Local arrangements:

David Aspinall, Edinburgh University, United Kingdom