coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Matthieu Sozeau <matthieu.sozeau AT inria.fr>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>, "types-announce AT lists.seas.upenn.edu" <types-announce AT lists.seas.upenn.edu>
Subject: [Coq-Club] CfP: Coq ITP Tutorial
Date: Tue, 07 Jul 2015 10:00:42 +0000

CALL FOR PARTICIPATION

Coq ITP Tutorial

August 27th-29th

Nanjing, China

================

You are invited to attend the Coq ITP Tutorial in Nanjing, China,

from the 27th of August to the 29th.

Audience

========

The tutorial is dedicated to beginners and should introduce to the

basics of the Coq proof assistant. The tutorial consists of a mixture of

lectures and practical classes where the participants are given

practical theorem problems to be solved in Coq.

Participants should bring their own laptops with Coq already installed

on it.

Speakers

========

Reynald Affeldt (AIST)

Sandrine Blazy (IRISA - University of Rennes 1)

Cyril Cohen (Inria - Marelle team)

Hugo Herbelin (Inria - πr2 team)

Gregory Malecha (Harvard University SEAS)

Enrico Tassi (Inria - Marelle team)

Program

=======

The program will address the basics of the Coq system, including:

- Propositions and proofs

- Programming in Coq

- Interactive proofs

- Proving properties of programs

- Datatypes / Inductive Datatypes / Recursion / Inductive Properties

Registration

============

Registration is part of the ITP'15 conference registration process.

Organizers

==========

Matthieu Sozeau (Inria - πr2 team)

Pierre-Yves Strub (IMDEA Software Institute)

(all information is also available at http://www.strub.nu/coq-itp-15)