# HG changeset patch # User Christian Urban # Date 1417219703 0 # Node ID 7b71e2c2b422c7ce590c34b8e2501c6695e00ebd # Parent b20c856b2389cde20f247ad8b9455409d2339b3a updated diff -r b20c856b2389 -r 7b71e2c2b422 cfp.pdf Binary file cfp.pdf has changed diff -r b20c856b2389 -r 7b71e2c2b422 cfp.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/cfp.tex Sat Nov 29 00:08:23 2014 +0000 @@ -0,0 +1,140 @@ +\documentclass{article} +\usepackage{times} +%\usepackage[latin1]{inputenc} +%\usepackage{fullpage} + +\addtolength{\textheight}{60mm} +\addtolength{\topmargin}{-30mm} +\addtolength{\textwidth}{70mm} +\addtolength{\oddsidemargin}{-35mm} + +\pagestyle{empty} +\parindent0em + +\begin{document} + +\begin{center} +\textbf{CALL FOR PAPERS}\\[1.2ex] +{\normalsize 6th International Conference on }\\[0.8ex] +{\large\bfseries Interactive Theorem Proving (ITP 2015)}\\[0.8ex] +{\normalsize\itshape 24 -- 27 August 2015, Nanjing, China}\\[1.2ex] +\texttt{http://www.inf.kcl.ac.uk/staff/urbanc/itp-2015/} +\end{center} + +\vspace{0mm} + +\begin{minipage}[t]{6.9cm}% first column +\renewcommand{\baselinestretch}{0.99}\parskip 4pt\small + +\textbf{Programme Committee:} \\ +Andrea Asperti, \emph{University of Bologna}\\ +Jesper Bengtson, \emph{IT University of Copenhagen}\\ +Steffen Berghofer, \emph{Secunet Security Networks AG}\\ +Yves Bertot, \emph{INRIA}\\ +Lars Birkedal, \emph{Aarhus University}\\ +Sandrine Blazy, \emph{IRISA}\\ +Thierry Coquand, \emph{University of Gothenburg}\\ +Xinyu Feng, \emph{Univ.~of Science and Technology of China}\\ +Ruben Gamboa, \emph{University of Wyoming}\\ +Herman Geuvers, \emph{Radboud University Nijmegen}\\ +Mike Gordon, \emph{Cambridge University}\\ +Elsa Gunter, \emph{University of Illinois, Urbana-Champaign}\\ +John Harrison, \emph{Intel Corporation}\\ +Hugo Herbelin, \emph{INRIA}\\ +Matt Kaufmann, \emph{University of Texas at Austin}\\ +Gerwin Klein, \emph{NICTA}\\ +Cesar Munoz, \emph{NASA Langley Research Center}\\ +Tobias Nipkow, \emph{TU M\"unchen}\\ +Michael Norrish, \emph{NICTA}\\ +Scott Owens, \emph{University of Kent}\\ +Randy Pollack, \emph{Edinburgh University}\\ +Carsten Sch\"urmann, \emph{IT University of Copenhagen}\\ +Konrad Slind, \emph{Rockwell Collins}\\ +Alwen Tiu, \emph{Nanyang Technological University}\\ +Christian Urban (co-chair), \emph{King's College London}\\ +Dimitrios Vytiniotis, \emph{Microsoft Research Cambridge}\\ +Xingyuan Zhang (co-chair), \emph{PLA University of Science and Technology Nanjing} +\\[1em] +% +\textbf{Important Dates:} \\ +\begin{tabular}{@{}l@{~~}r@{}} +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\\ +\end{tabular} +\\[1em] +\textbf{Organizers:} \\[1ex] +\begin{tabular}{@{}l@{}} +Xingyuan Zhang\\ +Chunhan Wu\\ +Christian Urban\\ +\end{tabular} + +\end{minipage} +\hspace{3mm} +\begin{minipage}[t]{11cm}% second column +\renewcommand{\baselinestretch}{0.95} +%\parskip0ex\parindent1.5em +\parskip1ex\parindent0em +%%%\small + +ITP is the premier international conference for researchers +from all areas of interactive theorem proving and its +applications. The sixth conference will be held on 24 through +27 August 2015 in Nanijing. + +{\bf Topics}\medskip + +The programme committee welcomes submissions on all aspects of +interactive theorem proving and its applications. The topics +include, but are not limited to, the following: + + +\begin{itemize} +\item Specification and verification of hardware: + microprocessors, memory systems, pipelines, etc; formal + semantics of hardware design languages; synthesis; + formal design flows. +\item Specification and verification of software: program + verification, refinement, and synthesis for functional, + declarative and imperative languages; formal semantics + of programming languages; proof carrying code. +\item Industrial application of theorem provers. +\item Formalization of mathematical theories. +\item Advances in theorem prover technology: proof automation + and decision procedures, induction, combination of + deductive and algorithmic approaches, incorporation of + theorem provers into larger systems, combination of + theorem provers with other provers and tools. +\item Other topics, including: security algorithms, + properties, and policies; specification and requirements + analysis of systems; user interfaces for theorem + provers; development and extension of higher order + logics. +\item Proof Pearls: concise and elegant presentations of + interesting examples. +\end{itemize} + +Submission is electronic. 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 LaTeX2e. The +proceedings are to be published as a volume in the Lecture +Notes in Computer Science series. + +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: 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. + +Authors of all accepted papers are expected to present their +paper at the conference. + + +\end{minipage} +\end{document} diff -r b20c856b2389 -r 7b71e2c2b422 index.html --- a/index.html Sat Nov 15 08:44:19 2014 +0000 +++ b/index.html Sat Nov 29 00:08:23 2014 +0000 @@ -107,18 +107,20 @@ - +

ITP 2015 will be in Nanjing

ITP 2015 will be in Nanjing, China

 TUM

-[CFP] +

+[Important Dates] +[CFP] [Conference History] -

+

The 6th conference on Interactive Theorem Proving will be held in -Nanjing. The organising committee is chaired by Xingyuan Zhang and Christian Urban. +Nanjing, China. The organising committee is chaired by Xingyuan Zhang and Christian Urban. Nanjing is situated in the heart of China — close to Shanghai and roughly equidistant between Beijing and Hong Kong. It is a former capital @@ -129,6 +131,13 @@ Series.

+

Important Dates

+Submission of title and abstract: 9 March 2015
+Submission of full paper: 13 March 2015
+Author notification: 15 May 2015
+Camera-ready papers: 5 June 2015
+Conference: 14-27 August 2015
+

Timing and Tentative Programme

The conference will be held in the last week of August (24th - 27th diff -r b20c856b2389 -r 7b71e2c2b422 pc --- a/pc Sat Nov 15 08:44:19 2014 +0000 +++ b/pc Sat Nov 29 00:08:23 2014 +0000 @@ -1,28 +1,54 @@ -Gerwin Klein (NICTA) -Ruben Gamboa (University of Wyoming) -Tobias Nipkow (TU Munich) -Michael Norrish (NICTA) -John Harrison (INTEL) -Thierry Coquand (University of Gothenburg) +Andrea Asperti (Uni Bologna) + http://www.cs.unibo.it/~asperti/ +Jesper Bengtson (IT University of Copenhagen) + http://www.itu.dk/people/jebe/ Steffen Berghofer (Secunet Security Networks AG) -Randy Pollack (Harvard University) -Mike Gordon (Cambridge University) -Sandrine Blazy (INRIA) -Herman Geuvers (Nijmegen) -Xinyu Feng (Suzhou Institute for Advanced Study) + http://wwwbroy.in.tum.de/~berghofe/ Yves Bertot (INRIA) -Konrad Slind (Rockwell Collins) + http://www-sop.inria.fr/members/Yves.Bertot/ +Lars Birkedal (Aarhus University) + http://cs.au.dk/~birke/ +Sandrine Blazy (IRISA) + https://www.irisa.fr/celtique/blazy/index.html#contact +Thierry Coquand (University of Gothenburg) + http://www.cse.chalmers.se/~coquand/ +Xinyu Feng (University of Science and Technology of China) + http://staff.ustc.edu.cn/~xyfeng/ +Ruben Gamboa (University of Wyoming) + http://www.cs.uwyo.edu/~ruben/ +Herman Geuvers (Nijmegen) + http://www.cs.ru.nl/~herman/ +Mike Gordon (Cambridge University) + https://www.cl.cam.ac.uk/~mjcg/ +Elsa Gunter (University of Illinois, Urbana - Champaign) + http://web.engr.illinois.edu/~egunter/ +John Harrison (Intel Corporation) + http://www.cl.cam.ac.uk/~jrh13/ Hugo Herbelin (INRIA) -Lars Birkedal (Aarhus) -Jesper Bengtson (ITU) -Carsten Schuermann (ITU) -Dimitrios Vytiniotis (Microsoft) -Elsa Gunter (Urbana Champain) -Cesar Munos (nasa) -Andrea Asperti (Uni Bologna) -Scott Owens (Kent) -Matt Kaufman (texas) -Alwen Tiu (Nanyang) + http://pauillac.inria.fr/~herbelin/index-eng.html +Matt Kaufman (University of Texas at Austin) + http://www.cs.utexas.edu/~kaufmann/ +Gerwin Klein (NICTA) + http://www.cse.unsw.edu.au/~kleing/ +Cesar Munoz (NASA Langley Research Center) + http://shemesh.larc.nasa.gov/people/cam/ +Tobias Nipkow (TU Munich) + http://www21.in.tum.de/~nipkow/ +Michael Norrish (NICTA) + http://nicta.com.au/people/norrishm +Scott Owens (University of Kent) + http://www.cs.kent.ac.uk/people/staff/sao/ +Randy Pollack (Harvard University) + http://homepages.inf.ed.ac.uk/rpollack/ +Carsten Schümann (IT University of Copenhagen) + http://www.itu.dk/people/carsten/ +Konrad Slind (Rockwell Collins) +Alwen Tiu (Nanyang Technological University) + http://www.ntu.edu.sg/home/atiu/ +Christian Urban (King's College London) +Dimitrios Vytiniotis (Microsoft Research Cambridge) + http://research.microsoft.com/en-us/people/dimitris/ +Xingyuan Zhang (PLA University of Science and Technology Nanjing) (25)