From mboxrd@z Thu Jan  1 00:00:00 1970
Date: Sun, 15 Oct 2017 15:45:17 -0700 (PDT)
From: Jeremy <jav...@gmail.com>
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Message-Id: <d9eb69ce-f1a2-4de1-8d5d-4528c096c571@googlegroups.com>
Subject: CFP: ITP 2018
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_22480_1999498897.1508107517398"

------=_Part_22480_1999498897.1508107517398
Content-Type: multipart/alternative; 
	boundary="----=_Part_22481_755558838.1508107517399"

------=_Part_22481_755558838.1508107517399
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable


                              FIRST CALL FOR PAPERS

                                    ITP 2018
          9th International Conference on Interactive Theorem Proving
                                   Oxford, UK
                                 July 9-12, 2018
                            https://itp2018.inria.fr/


Submission Deadlines: Thursday,  January 25, 2018 (abstracts)
                      Wednesday, January 31, 2018 (full papers)

GENERAL INFORMATION
The ITP conference series is concerned with all topics related to=20
interactive
theorem proving, ranging from theoretical foundations to implementation=20
aspects
and applications in program verification, security, and formalization of
mathematics. ITP is the evolution of the TPHOLs conference series to the=20
broad
field of interactive theorem proving. TPHOLs meetings took place every year=
=20
from
1988 until 2009. The ninth ITP conference, ITP 2018, will be held in Oxford=
,
July 9-12, 2018.

SCOPE OF CONFERENCE
ITP welcomes submissions describing original research on all aspects of
interactive theorem proving and its applications. Suggested topics include=
=20
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
*  concise and elegant worked examples of formalizations (proof pearls)

PUBLICATION DETAILS
The proceedings of the symposium will be published in the Springer's LNCS
series.

PAPER SUBMISSIONS
All submissions must be original, unpublished, and not submitted=20
concurrently
for publication elsewhere. Furthermore, when appropriate, submissions are
expected to be accompanied by verifiable evidence of a suitable=20
implementation,
such as the source files of a formalization for the proof assistant used.=
=20
These
materials can be uploaded with the submission, or made available on the=20
web. In
either case, the submission should provide clear instructions to referees=
=20
as to
how to obtain the relevant materials and compile them or check them, as the=
=20
case
may be.

Submissions will be subjected to single-blind peer review. They should be n=
o
more than 16 pages in length excluding bibliographic references and are to=
=20
be
submitted in PDF via EasyChair at the following address:

  https://easychair.org/conferences/?conf=3Ditp2018

Submissions must conform to the LNCS style in LaTeX. An author of each=20
accepted
paper is expected to present it at the conference and will be required to=
=20
sign a
copyright release form.

In addition to regular papers, described above, there will be a section for
shorter papers, which can be used to describe interesting work that is stil=
l
ongoing and not fully mature. Such a preliminary report is limited to 6=20
pages
and may consist of an extended abstract. Each of these papers should bear=
=20
the
phrase "(short paper)" beneath the title, and will be refereed and be=20
expected
to present innovative and promising ideas, possibly in early form. Accepted
submissions in this category will be published in the main proceedings and=
=20
will
be presented as short talks.

IMPORTANT DATES
Abstract submission deadline: January 25, 2018
Full paper submission deadline: January 31, 2018
Author notification: March 31, 2018
Camera-ready papers: May 2, 2018
Conference: July 9-10, 2018

PROGRAM COMMITTEE
Jeremy Avigad, Carnegie Mellon University (chair)
Assia Mahboubi, Inria (chair)
Andreas Abel, Gothenburg University
Benedikt Ahrens, University of Birmingham
June Andronick, CSIRO|Data61 and UNSW
Adam Chlipala, Massachusetts Institute of Technology
Jasmin Christian Blanchette, Vrije Universiteit Amsterdam
Thierry Coquand, Chalmers University of Technology
Karl Crary, Carnegie Mellon University
Delphine Demange, IRISA / University of Rennes 1
Timothy Griffin, University of Cambridge
Thomas Hales, University of Pittsburgh
John Harrison, Intel
Johannes H=C3=B6lzl, Vrije Universiteit Amsterdam
Chung-Kil Hur, Seoul National University
Jacques-Henri Jourdan, LRI, CNRS, Universit=C3=A9 Paris-Sud
Cezary Kaliszyk, University of Innsbruck
Ambrus Kaposi, E=C3=B6tv=C3=B6s Lor=C3=A1nd University, Budapest
Chantal Keller, LRI, CNRS, Universit=C3=A9 Paris-Sud
Panagiotis Manolios, Northeastern University
Mariano Moscato, National Institute of Aerospace
Leonardo de Moura, Microsoft Research
Magnus O. Myreen, Chalmers University of Technology
Tobias Nipkow, Technische Universit=C3=A4t M=C3=BCnchen
Lawrence Paulson, University of Cambridge
Andr=C3=A9 Platzer, Carnegie Mellon University
Andrei Popescu, Middlesex University London
Matthieu Sozeau, Inria
Pierre-Yves Strub, =C3=89cole Polytechnique
Enrico Tassi, Inria
Zachary Tatlock, University of Washington
Laurent Th=C3=A9ry, Inria
Cesare Tinelli, The University of Iowa
Alwen Tiu, Australian National University
Makarius Wenzel, sketis.net
Freek Wiedijk, Radboud University Nijmegen

CONTACT INFORMATION
Jeremy Avigad
Assia Mahboubi
itp...@easychair.org
https://itp2018.inria.fr/


------=_Part_22481_755558838.1508107517399
Content-Type: text/html; charset=utf-8
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><div><br></div><div>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=
=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 FIRST CA=
LL FOR PAPERS</div><div><br></div><div>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=
=A0 =C2=A0 =C2=A0 ITP 2018</div><div>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 9th=
 International Conference on Interactive Theorem Proving</div><div>=C2=A0 =
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=
=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0Oxford, UK</div><div>=C2=A0 =
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=
=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0July 9-12, 2018</div><div>=C2=A0 =C2=
=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =
=C2=A0 =C2=A0 https://itp2018.inria.fr/</div><div><br></div><div><br></div>=
<div>Submission Deadlines: Thursday, =C2=A0January 25, 2018 (abstracts)</di=
v><div>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=
=A0 =C2=A0 Wednesday, January 31, 2018 (full papers)</div><div><br></div><d=
iv>GENERAL INFORMATION</div><div>The ITP conference series is concerned wit=
h all topics related to interactive</div><div>theorem proving, ranging from=
 theoretical foundations to implementation aspects</div><div>and applicatio=
ns in program verification, security, and formalization of</div><div>mathem=
atics. ITP is the evolution of the TPHOLs conference series to the broad</d=
iv><div>field of interactive theorem proving. TPHOLs meetings took place ev=
ery year from</div><div>1988 until 2009. The ninth ITP conference, ITP 2018=
, will be held in Oxford,</div><div>July 9-12, 2018.</div><div><br></div><d=
iv>SCOPE OF CONFERENCE</div><div>ITP welcomes submissions describing origin=
al research on all aspects of</div><div>interactive theorem proving and its=
 applications. Suggested topics include but</div><div>are not limited to th=
e following:</div><div><br></div><div>* =C2=A0formal aspects of hardware an=
d software</div><div>* =C2=A0formalizations of mathematics</div><div>* =C2=
=A0improvements in theorem prover technology</div><div>* =C2=A0user interfa=
ces for interactive theorem provers</div><div>* =C2=A0formalizations of com=
putational models</div><div>* =C2=A0verification of security algorithms</di=
v><div>* =C2=A0use of theorem provers in education</div><div>* =C2=A0indust=
rial applications of interactive theorem provers</div><div>* =C2=A0concise =
and elegant worked examples of formalizations (proof pearls)</div><div><br>=
</div><div>PUBLICATION DETAILS</div><div>The proceedings of the symposium w=
ill be published in the Springer&#39;s LNCS</div><div>series.</div><div><br=
></div><div>PAPER SUBMISSIONS</div><div>All submissions must be original, u=
npublished, and not submitted concurrently</div><div>for publication elsewh=
ere. Furthermore, when appropriate, submissions are</div><div>expected to b=
e accompanied by verifiable evidence of a suitable implementation,</div><di=
v>such as the source files of a formalization for the proof assistant used.=
 These</div><div>materials can be uploaded with the submission, or made ava=
ilable on the web. In</div><div>either case, the submission should provide =
clear instructions to referees as to</div><div>how to obtain the relevant m=
aterials and compile them or check them, as the case</div><div>may be.</div=
><div><br></div><div>Submissions will be subjected to single-blind peer rev=
iew. They should be no</div><div>more than 16 pages in length excluding bib=
liographic references and are to be</div><div>submitted in PDF via EasyChai=
r at the following address:</div><div><br></div><div>=C2=A0 https://easycha=
ir.org/conferences/?conf=3Ditp2018</div><div><br></div><div>Submissions mus=
t conform to the LNCS style in LaTeX. An author of each accepted</div><div>=
paper is expected to present it at the conference and will be required to s=
ign a</div><div>copyright release form.</div><div><br></div><div>In additio=
n to regular papers, described above, there will be a section for</div><div=
>shorter papers, which can be used to describe interesting work that is sti=
ll</div><div>ongoing and not fully mature. Such a preliminary report is lim=
ited to 6 pages</div><div>and may consist of an extended abstract. Each of =
these papers should bear the</div><div>phrase &quot;(short paper)&quot; ben=
eath the title, and will be refereed and be expected</div><div>to present i=
nnovative and promising ideas, possibly in early form. Accepted</div><div>s=
ubmissions in this category will be published in the main proceedings and w=
ill</div><div>be presented as short talks.</div><div><br></div><div>IMPORTA=
NT DATES</div><div>Abstract submission deadline: January 25, 2018</div><div=
>Full paper submission deadline: January 31, 2018</div><div>Author notifica=
tion: March 31, 2018</div><div>Camera-ready papers: May 2, 2018</div><div>C=
onference: July 9-10, 2018</div><div><br></div><div>PROGRAM COMMITTEE</div>=
<div>Jeremy Avigad, Carnegie Mellon University (chair)</div><div>Assia Mahb=
oubi, Inria (chair)</div><div>Andreas Abel, Gothenburg University</div><div=
>Benedikt Ahrens, University of Birmingham</div><div>June Andronick, CSIRO|=
Data61 and UNSW</div><div>Adam Chlipala, Massachusetts Institute of Technol=
ogy</div><div>Jasmin Christian Blanchette, Vrije Universiteit Amsterdam</di=
v><div>Thierry Coquand, Chalmers University of Technology</div><div>Karl Cr=
ary, Carnegie Mellon University</div><div>Delphine Demange, IRISA / Univers=
ity of Rennes 1</div><div>Timothy Griffin, University of Cambridge</div><di=
v>Thomas Hales, University of Pittsburgh</div><div>John Harrison, Intel</di=
v><div>Johannes H=C3=B6lzl, Vrije Universiteit Amsterdam</div><div>Chung-Ki=
l Hur, Seoul National University</div><div>Jacques-Henri Jourdan, LRI, CNRS=
, Universit=C3=A9 Paris-Sud</div><div>Cezary Kaliszyk, University of Innsbr=
uck</div><div>Ambrus Kaposi, E=C3=B6tv=C3=B6s Lor=C3=A1nd University, Budap=
est</div><div>Chantal Keller, LRI, CNRS, Universit=C3=A9 Paris-Sud</div><di=
v>Panagiotis Manolios, Northeastern University</div><div>Mariano Moscato, N=
ational Institute of Aerospace</div><div>Leonardo de Moura, Microsoft Resea=
rch</div><div>Magnus O. Myreen, Chalmers University of Technology</div><div=
>Tobias Nipkow, Technische Universit=C3=A4t M=C3=BCnchen</div><div>Lawrence=
 Paulson, University of Cambridge</div><div>Andr=C3=A9 Platzer, Carnegie Me=
llon University</div><div>Andrei Popescu, Middlesex University London</div>=
<div>Matthieu Sozeau, Inria</div><div>Pierre-Yves Strub, =C3=89cole Polytec=
hnique</div><div>Enrico Tassi, Inria</div><div>Zachary Tatlock, University =
of Washington</div><div>Laurent Th=C3=A9ry, Inria</div><div>Cesare Tinelli,=
 The University of Iowa</div><div>Alwen Tiu, Australian National University=
</div><div>Makarius Wenzel, sketis.net</div><div>Freek Wiedijk, Radboud Uni=
versity Nijmegen</div><div><br></div><div>CONTACT INFORMATION</div><div>Jer=
emy Avigad</div><div>Assia Mahboubi</div><div>itp...@easychair.org</div><di=
v>https://itp2018.inria.fr/</div><div><br></div></div>
------=_Part_22481_755558838.1508107517399--

------=_Part_22480_1999498897.1508107517398--