CALL FOR PAPERS

                              Special Issue On 

                  MILESTONES IN INTERACTIVE THEOREM PROVING

                       Journal of Automated Reasoning


The past few decades have seen major achievements in interactive theorem
proving, such as the formalisation of deep mathematical theorems and
significant bodies of theoretical computer science, as well as the
verification of complex software and hardware systems. Too often, these
impressive results have been published in abbreviated or fragmentary form in
conference proceedings, or not at all. This special issue welcomes
full-length papers describing past work not previously published in a
journal, along with new developments of any length. Small, self-contained
Proof Pearls and applications of all kinds are also welcome.

This special issue will be devoted to applications of interactive theorem
proving in their full variety: formalised mathematics, formalised theory,
formalised semantics, formal proofs of hardware or software systems. They can
be large or small.

Manuscripts should be unpublished works and not submitted elsewhere. Revised
and enhanced versions of papers published in conference proceedings that have
not appeared in archival journals are eligible for submission. All
submissions will be reviewed according to the usual standards of scholarship
and originality.

Papers should be in pdf format, following the JAR guidelines for authors, and
be submitted using the usual Springer online submission system:
           http://www.editorialmanager.com/jars/default.aspx

When you reach the drop-down menu "Choose Article Type", you must select
"S.I. : MILESTONE" to specify the special issue.. To encourage a speedy
review cycle, it will be expected that authors of submissions also serve as
referees.

Important Dates
1 Apr 2017    Submission Deadline
1 Oct 2017    Notification of accepted papers
1 Jan 2018    Final version

For more information, please see
               http://www.cse.unsw.edu.au/~kleing/JAR-milestone/


Guest Editors
  Larry Paulson, University of Cambridge
  Jeremy Avigad, Carnegie Mellon University
  Gerwin Klein, Data61 and UNSW Australia