ISABELLE 2014 PAPERS (UNREFEREED): EDITOR'S PREFACE

These are the proceedings of Isabelle 2014, a workshop bringing together users and developers of the Isabelle theorem prover. It was held on 12/7/2014 as part of the Vienna Summer of Logic (VSL 2014).

The 13 papers presented at the workshop were not formally refereed; they were merely discussed informally among the editors. Although the workshop is intended as a forum for presenting preliminary results and work in progress, some of the papers are of exceptional quality and we expect them to appear in major conferences or journals soon.

We had always intended to include an Isabelle tutorial as part of the programme. The unexpectedly high number of submissions left us with a choice between parallel sessions and a highly compressed timetable. We chose the former option, conducting the tutorial separately from the morning workshop sessions. The tutorial material is also part of the proceedings (in directory frontmatter).

We are grateful to the VSL 2014 organisers and sponsors, who created an environment in which we could set up our workshop easily. We generated these proceedings and the conference programme using EasyChair. In parallel to EasyChair we used the experimental conference management system CoCon. The core of CoCon is generated from Isabelle/HOL where certain confidentiality guarantees have been proved about CoCon (see the CAV 2014 paper by Kanav, Lammich and Popescu entitled A Conference Management System with Verified Document Confidentiality).