The Coq mailing list

[Viktor Vafeiadis <viktor AT mpi-sws.org>]

The 6th Coq Workshop
July 18, 2014 · Vienna, Austria

http://vsl2014.at/pages/Coq-index.html

The Coq Workshop series brings together Coq users, developers, and 
contributors.  While conferences like ITP provide a venue for traditional 
research papers, the Coq Workshop focuses on strengthening the Coq community 
and providing a forum for discussing practical issues, including the future 
of the Coq software and its associated ecosystem of libraries and tools.  
Thus, the workshop will be organized around informal presentations and 
discussions, supplemented with invited talks.

=== REGISTRATION === 

Registration is via the VSL'14 website. When registering, please select the 
Coq workshop as the event you are registering for.

Registration URL: http://vsl2014.at/registration/
Registration fee: 100 EUR (before June 8); 120 EUR (before June 30); 130 EUR 
(afterwards) 
Early registration deadline: ** 8 June 2014 **

=== SCHEDULE ===

08:45 New and advanced Coq features
* Presentation of Three Neat Tricks in Coq 8.5 (J. Gross)
* Towards a better-behaved unification algorithm for Coq (B. Ziliani and M. 
Sozeau)
* Proof-relevant rewriting strategies in Coq (M. Sozeau)

10:15 Coffee break

10:45 Invited talk
* Dan Licata: What is Homotopy Type Theory? 

11:45 Useful tools
* QuickChick: Property-Based Testing for Coq (M. Dénès, C. Hritcu, L. 
Lampropoulos, Z. Paraskevopoulou and B. C. Pierce)
* Proof-Pattern Search in Coq/SSReflect (J. Heras and E. Komendantskaya)

12:45 Lunch break

14:30 Formalizations in Coq 
* Formalization of Error-correcting Codes using SSReflect (R. Affeldt and J. 
Garrigue)
* Autosubst: Automation for de Bruijn Substitutions (S. Schäfer, T. Tebbi and 
G. Smolka)
* Automating Abstract Logics (G. Malecha, J. Bengtson and A. Chlipala)
  
16:00 Coffee break

16:30 New IDEs and Coq 8.5 update
* Asynchronous interaction for Coq (C. Tankink)
* Coqoon: towards a modern IDE for Coq (A. Faithfull and J. Bengtson)
* Coq 8.5 update (M. Sozeau)

Abstracts for these talks can be found at 
http://vsl2014.at/pages/Coq-program.html