[TYPES] *** Coq survey *** (DEADLINE January 15th)

Derek Dreyer dreyer at mpi-sws.org
Tue Dec 24 18:41:11 EST 2013

[Matthieu Sozeau asked me to post this to the Types list on behalf of
the Coq team.  The results of the survey linked below will play a role
in determining the future directions for development of Coq, so if you
care about that, I encourage you to take time to fill it out. -Derek]

Dear all,

 on behalf of the Coq developers, I’d like to invite everyone to respond
to a survey on their usage of Coq, its programming and proving
environment, development model, shortcomings and future directions. This
survey aims at gathering important information about Coq's users and
uses. The results will be used to better understand users' needs, and
help decide in which direction Coq’s development should go. It is really
important for us to get as many answers as possible before *** January
15th 2014 ***. We are also taking this occasion to collaboratively build
a bibliography of Coq-related papers. The survey’s results will be
synthesized, anonymized and made publicly available in february.

 The estimated burden time for this survey is around 30 minutes. The
survey is available online at:


 This survey was mainly prepared by Thomas Braibant, assisted by Enrico
Tassi, thanks to them for giving us all an occasion to take a step back
and reflect on Coq’s future.

Happy holidays,
— Matthieu, for the Coq team.

More information about the Types-list mailing list