Call for Papers

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:

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

Guest Editors

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

Last updated: 17 Aug 2016.