The Coq mailing list

[Arthur Charguéraud <arthur.chargueraud AT inria.fr>]

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

                         PROGRAM FOR

                         CoqPL 2016

                  2nd International Workshop on
                  Coq for Programming Languages
                              --
             January, 23rd 2016, co-located with POPL
              St. Petersburg, Florida, United States

http://conf.researchr.org/home/CoqPL-2016
====================================================================


Dear all,

Here is the description of the program for the workshop.


CoqPL will feature two invited talks:

*) Coq 8.5 at work and the future of Coq
       by Matthieu Sozeau.

*) A Tutorial on using the Paco Library for coinductive reasoning
      by Chung-Kil Hur.


The main program of CoqPL will consists of eight talks:

*) A Coq Library for Binary Logical Relations
      by Jérémie Koenig.

*) A Coinduction Proof Rule for Hoare Doubles
      by Christian J. Bell and Adam Chlipala.

*) Company-Coq: Taking Proof General one step closer to a real IDE
      by Clément Pit-Claudel and Pierre Courtieu.

*) Certified Desugaring of Javascript Programs using Coq
      by Marek Materzok.

*) Formal Verification of Stability Properties of Cyber-Physical Systems
      by Matthew Chan, Daniel Ricketts, Sorin Lerner and Gregory Malecha.

*) The Category-theoretic Solution of Recursive Ultra-metric Space Equations
      by Amin Timany and Bart Jacobs.

*) Formalizing Simple Refinements in Coq
      by Nico Lehmann and Éric Tanter.

*) A Case for Tactics with (Limited) Side Effects
      by Benjamin Delaware.


(The exact schedule will be provided later.)



Looking forward to seeing you there!

Best,

Arthur Charguéraud
PC chair for CoqPL'2016