The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

Out of curiosity, I may be missing the current one, but is there any
resource that systematically attempts to collect the more advanced
features of Coq?  As an example, while working through SF and CPDT
will teach you a lot, when you hop into real developments you need to
learn a laundry list of other things, such as libraries (Penn's
metatheory library, SSReflect, etc...), lesser documented features
(type classes and coercions), and new theory (e.g., working with the
homotopy type theory branch).

Cocorico is a fairly good resource:

http://coq.inria.fr/cocorico/

But it's unclear to me whether it's been kept current so that people
can systematically progress from beginner to advanced feature users.
(Usually the advanced features are just sugar on top of core concepts,
e.g., dependent sums in the case of records and type classes.).  It
would be nice to see this addressed somewhere, since while SF/CPDT are
certainly great texts, they don't tell the full story if you want to
work with real world Coq code.

Kris


On Tue, Feb 11, 2014 at 6:54 PM, Greg Morrisett 
<greg AT eecs.harvard.edu>
 wrote:
> The Oregon Summer School on Programming Languages will offer
> a "bootcamp" on Coq (amongst other topics) this summer:
>
>   https://www.cs.uoregon.edu/research/summerschool/summer14/
>
> There are also great texts, such as "Software Foundations" and
> "Certified Programming with Dependent Types" that can teach
> you a lot on your own.
>
> For more detailed technical research, there is the Coq workshop
> that will happen as part of ITP this summer (I presume).
>
> Hope this helps,
>
> -Greg
>
> On Feb 11, 2014, at 10:00 AM, Sebastien 
> <fricker AT froglogic.com>
>  wrote:
>
>> Hi,
>> does anybody know if there is COQ workshop planed or are there any 
>> training existing for COQ?
>> Sébastien
>