[TYPES/announce] CFP for ITP 2015

[Christian Urban]

CALL FOR PAPERS: ITP 2015

The 6th International Conference on Interactive Theorem Proving

24 - 27 August 2015 in Nanjing, China


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.

 *****************************************************
 *  http://www.inf.kcl.ac.uk/staff/urbanc/itp-2015/  *
 *****************************************************


Important Dates
---------------
Title & Abstract Submission:  9 March 2015
Full Paper Submission:       13 March 2015 
Author Notification:           15 May 2015
Camera-Ready Papers due:       5 June 2015
Conference:            24 - 27 August 2015
Submission Page:       https://easychair.org/conferences/?conf=itp2015

Topics
------

ITP welcomes submissions describing original research on all aspects
of interactive theorem proving and its applications. 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,
- verification of security algorithms,
- use of theorem provers in education,
- industrial applications of interactive theorem provers, and
- concise and elegant worked examples of formalizations ("Proof Pearls").

Papers should be no more than 16 pages in length and are to be
submitted in PDF format. They must conform to the LNCS style
preferably using LaTeX. The proceedings are to be published as a
volume in the Lecture Notes in Computer Science series and will be
available to participants at the conference.

Authors of accepted papers are expected to present their paper at the
conference.

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


Programme Committee
-------------------

Andrea Asperti       University of Bologna, Italy
Jesper Bengtson      IT University of Copenhagen, Denmark
Stefan Berghofer     Secunet Security Networks AG, Germany
Yves Bertot          INRIA, France
Lars Birkedal        Aarhus University, Denmark
Sandrine Blazy       University of Rennes, France
Bob Constable        Cornell University, USA
Thierry Coquand      University of Gothenburg, Sweden
Xinyu Feng           University of Science and Technology, China
Ruben Gamboa         University of Wyoming, USA
Herman Geuvers       Radboud University Nijmegen, The Netherlands
Mike Gordon          Cambridge University, United Kingdom
Elsa Gunter          University of Illinois, Urbana-Champaign, USA
John Harrison        Intel Corporation, USA
Hugo Herbelin        INRIA, France
Matt Kaufmann        University of Texas at Austin, USA
Gerwin Klein         NICTA, Australia
Cesar Munoz          NASA Langley Research Center, USA
Tobias Nipkow        TU München, Germany
Michael Norrish      NICTA, Australia
Scott Owens          University of Kent, United Kingdom
Randy Pollack        Harvard University, USA
Carsten Schürmann    IT University of Copenhagen, Denmark
Konrad Slind         Rockwell Collins, USA
Alwen Tiu            Nanyang Technological University, Singapore
Christian Urban      King's College London, United Kingdom (co-chair)
Dimitrios Vytiniotis Microsoft Research Cambridge, United Kingdom
Xingyuan Zhang 	     PLA University of Science and Technology, China (co-chair)


Organizers
----------

Xingyuan Zhang 
Chunhan Wu 
Jinshang Wang 
Christian Urban