The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

       Mathematical Components, an Introduction
      Satellite workshop of the ITP 2016 conference
             August 27th, Nancy, France
  https://github.com/math-comp/wiki/wiki/tutorial-itp2016


Mathematical Components (https://math-comp.github.io/math-comp/) 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 main ingredients used throughout
these large scale 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.

Lectures will present the Ssreflect tactic language, principles of the boolean
reflection methodology and provide a guided tour through a sample of libraries
and data structures: finite graphs, iterated operators, matrices...

Participants are required to bring a laptop with a recent browser installed
(see the test link on the tutorial webpage).

Registration at https://itp2016.inria.fr/registration/
-- 
Assia Mahboubi, Enrico Tassi