27 \renewcommand{\baselinestretch}{0.99}\parskip 4pt\small |
27 \renewcommand{\baselinestretch}{0.99}\parskip 4pt\small |
28 |
28 |
29 \textbf{Programme Committee:} \\ |
29 \textbf{Programme Committee:} \\ |
30 Andrea Asperti, \emph{University of Bologna}\\ |
30 Andrea Asperti, \emph{University of Bologna}\\ |
31 Jesper Bengtson, \emph{IT University of Copenhagen}\\ |
31 Jesper Bengtson, \emph{IT University of Copenhagen}\\ |
32 Steffen Berghofer, \emph{Secunet Security Networks AG}\\ |
32 Stefan Berghofer, \emph{Secunet Security Networks AG}\\ |
33 Yves Bertot, \emph{INRIA}\\ |
33 Yves Bertot, \emph{INRIA}\\ |
34 Lars Birkedal, \emph{Aarhus University}\\ |
34 Lars Birkedal, \emph{Aarhus University}\\ |
35 Sandrine Blazy, \emph{IRISA}\\ |
35 Sandrine Blazy, \emph{IRISA}\\ |
36 Thierry Coquand, \emph{University of Gothenburg}\\ |
36 Thierry Coquand, \emph{University of Gothenburg}\\ |
37 Xinyu Feng, \emph{Univ.~of Science and Technology of China}\\ |
37 Xinyu Feng, \emph{Univ.~of Science and Technology of China}\\ |
51 Carsten Sch\"urmann, \emph{IT University of Copenhagen}\\ |
51 Carsten Sch\"urmann, \emph{IT University of Copenhagen}\\ |
52 Konrad Slind, \emph{Rockwell Collins}\\ |
52 Konrad Slind, \emph{Rockwell Collins}\\ |
53 Alwen Tiu, \emph{Nanyang Technological University}\\ |
53 Alwen Tiu, \emph{Nanyang Technological University}\\ |
54 Christian Urban (co-chair), \emph{King's College London}\\ |
54 Christian Urban (co-chair), \emph{King's College London}\\ |
55 Dimitrios Vytiniotis, \emph{Microsoft Research Cambridge}\\ |
55 Dimitrios Vytiniotis, \emph{Microsoft Research Cambridge}\\ |
56 Xingyuan Zhang (co-chair), \emph{PLA University of Science and Technology Nanjing} |
56 Xingyuan Zhang (co-chair), \emph{PLA University of Science and Technology} |
57 \\[1em] |
57 \\[1em] |
58 % |
58 % |
59 \textbf{Important Dates:} \\ |
59 \textbf{Important Dates:} \\ |
60 \begin{tabular}{@{}l@{~~}r@{}} |
60 \begin{tabular}{@{}l@{~~}r@{}} |
61 Title \& abstract submission: & 9 March 2015\\ |
61 Title \& abstract submission: & 9 March 2015\\ |
81 %%%\small |
81 %%%\small |
82 |
82 |
83 ITP is the premier international conference for researchers |
83 ITP is the premier international conference for researchers |
84 from all areas of interactive theorem proving and its |
84 from all areas of interactive theorem proving and its |
85 applications. The sixth conference will be held on 24 through |
85 applications. The sixth conference will be held on 24 through |
86 27 August 2015 in Nanijing. |
86 27 August 2015 in Nanjing.\medskip |
87 |
87 |
88 {\bf Topics}\medskip |
88 {\bf Topics}\medskip |
89 |
89 |
90 The programme committee welcomes submissions on all aspects of |
90 The programme committee welcomes submissions on all aspects of |
91 interactive theorem proving and its applications. The topics |
91 interactive theorem proving and its applications. The topics |
106 \item Advances in theorem prover technology: proof automation |
106 \item Advances in theorem prover technology: proof automation |
107 and decision procedures, induction, combination of |
107 and decision procedures, induction, combination of |
108 deductive and algorithmic approaches, incorporation of |
108 deductive and algorithmic approaches, incorporation of |
109 theorem provers into larger systems, combination of |
109 theorem provers into larger systems, combination of |
110 theorem provers with other provers and tools. |
110 theorem provers with other provers and tools. |
111 \item Other topics, including: security algorithms, |
111 \item Other topics, including formal verification of security |
112 properties, and policies; specification and requirements |
112 policies and configurations (formal analysis, |
113 analysis of systems; user interfaces for theorem |
113 verification of security algorithms, etc); specification |
114 provers; development and extension of higher order |
114 and requirements analysis of systems; user interfaces |
115 logics. |
115 for theorem provers; development and extension of higher |
|
116 order logics. |
116 \item Proof Pearls: concise and elegant presentations of |
117 \item Proof Pearls: concise and elegant presentations of |
117 interesting examples. |
118 interesting examples. |
118 \end{itemize} |
119 \end{itemize} |
119 |
120 |
120 Submission is electronic. Papers should be no more than 16 |
121 Submission is electronic. Papers should be no more than 16 |