The following workshops will be co-located with ITP 2016.
(The HOL Workshop 2016 has been canceled.)
Coq Workshop 2016 26 August
Organizers: Julien Narboux and Nicolas Magaud (University of Strasbourg).
The Coq Workshop brings together Coq users, developers, and contributors. The Coq Workshop focuses on strengthening the Coq community and providing a forum for discussing practical issues, including the future of the Coq software and its associated ecosystem of libraries and tools. Thus, the workshop will be organized around informal presentations and discussions, supplemented with invited talks. This series of events was started in 2009.
See the workshop web site for details.
Isabelle Workshop 2016 25 August (afternoon) and 26 August (morning)
Organizers: Tobias Nipkow (Technische Universität München), Lawrence C. Paulson (University of Cambridge), and Makarius Wenzel.
This informal workshop will bring together Isabelle users and developers. Participants are invited to present their research and projects, including applications of Isabelle, internal developments, add-on tools, and reports on work in progress. Isabelle workshops have been held at irregular intervals for more than a decade, usually associated with international conferences (e.g. CADE 2007, TPHOLs 2009, ITP 2012, and ITP 2014).
See the workshop web site for details.
Mathematical Components, an Introduction 27 August
Organizers: Assia Mahboubi (Inria Saclay – Île-de-France) and Enrico Tassi (Inria Sophia Antipolis – Méditerranée).
Mathematical Components is the name of a Coq library covering a variety of topics, from the theory of basic data structures (e.g., numbers, lists, finite sets) to advanced results in various flavors of algebra. This library constitutes the infrastructure for the formal proofs of the Four Color Theorem and of the Odd Order Theorem. The aim of this tutorial is to present the ingredients used throughout this development, like the Ssreflect proof language or small scale reflection methods, and the basic libraries of general interest. The schedule will interleave small lectures by developers and advanced users of the library with supervised hands-on sessions. The intended audience is both people familiar with Coq but not with the Mathematical Components libraries and people with a background in proof assistants but not regular users of Coq.
See the tutorial web site for details.
