[TYPES/announce] CfP: Coq ITP Tutorial

[Matthieu Sozeau]

                     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)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20150707/afe8bb9e/attachment.html>